Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois tech talk: Verifying C programs in Coq using VST</h1> <div class='date'><time class="dtstart dt-start" title="2014-08-08T11:00:00" datetime="2014-08-08T11:00:00">Friday, August 8, 2014 from 11am</time>–<time class="dtend dt-end" title="2014-08-08T12:00:00" datetime="2014-08-08T12:00:00">noon</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><strong>abstract:</strong> C programs are notoriously difficult to reason about, either for safety or full functional correctness. Even with a program logic powerful enough to prove the necessary properties, the proof has the assumption that the compiler behaves exactly the way it is expected to. Verified Software Toolchain (VST) answers this problem by providing a logic specified at the source level that proves properties about generated assembly code. It is proved sound w.r.t. the operational semantics of C, the same operational semantics compiled by the proved-correct CompCert verified optimizing C compiler. Both of those proofs are machine-checked in Coq, an interactive proof assistant. This talk will present the basics of VST, followed by an example proof of a C program.</p> <p><strong>bio:</strong> Josiah (Joey) Dodds is an intern at Galois for the summer, researching the verification of cryptographic libraries. After the summer he will return to finish his PhD at Princeton, where he has been verifying information-flow properties and C programs in Coq.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://galois.com/blog/2014/07/tech-talk-verifying-c-programs-coq-using-vst/">Website</a></li> </ul> </div>