Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois tech talk: The CH2O project: making sense of the C standard</h1> <div class='date'><time class="dtstart dt-start" title="2015-06-18T10:00:00" datetime="2015-06-18T10:00:00">Thursday, June 18, 2015 from 10</time>–<time class="dtend dt-end" title="2015-06-18T11:00:00" datetime="2015-06-18T11:00:00">11am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>abstract:</p> <p>CH2O is the PhD project of Robbert Krebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fundamentally inconsistent.</p> <p>There are three versions of the CH2O semantics: a (small step) operational semantics, an executable semantics, and an axiomatic semantics (a separation logic for C). The most important properties — soundness and completeness results, subject reduction and progress, correctness of the type checker — have all been proved. All definitions and proofs have been fully formalized in Coq, without any axioms and on top of a non-trivial support library.</p> <p>The CH2O project has two abstract C-like languages. A significant subset of C called “CH2O abstract C” is translated into a simplified language called “CH2O core C”. This translation is written in Coq and implicitly gives a semantics to CH2O abstract C. The rest of the formalization is all about CH2O core C.</p> <p>The executable CH2O semantics has been extracted to OCaml and combined with the CIL parser to a standalone “interpreter”. This tool can be used to explore all behaviors of a program according to the C standard. Although the CH2O semantics does not yet support I/O (nor the exit function), a small hack allows the CH2O interpreter to still explore programs that call printf.</p> <p>The CH2O semantics has been specifically designed to be compatible with the CompCert semantics for C. Significant differences between CompCert and CH2O are that the CH2O semantics has explicit typing judgments for everything, and that CH2O applies to any ISO compliant compiler.</p> <p>bio:</p> <p>I have a master degree in mathematics (my thesis was about conformal supergravity), and a PhD in computer science, both from the University of Amsterdam. I also worked as a system administrator at the University of Utrecht.</p> <p>Currently I’m an assistant professor of computer science at the Radboud University Nijmegen. My research has been mainly about formalization of mathematics using interactive theorem provers, but recently I have been getting interested in practical program verification, where interactive proof is used when automation doesn’t cut it.</p> <p>At the moment I am an alternate member of WG14, and I won a price in the IOCCC twice. And my favorite project is the CakeML/verified-HOL Light project.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://galois.com/blog/2015/06/tech-talk-ch2o-project-making-sense-c-standard/">Website</a></li> </ul> </div>