Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: Automatic Function Annotations for Hoare Logic</h1> <div class='date'><time class="dtstart dt-start" title="2013-02-12T10:30:00" datetime="2013-02-12T10:30:00">Tuesday, February 12, 2013 from 10:30</time>–<time class="dtend dt-end" title="2013-02-12T11:30:00" datetime="2013-02-12T11:30:00">11:30am</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>Presented by Daniel Matichuk.</p> <p>Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a side-condition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="https://corp.galois.com/blog/2013/2/6/tech-talk-automatic-function-annotations-for-hoare-logic.html">Website</a></li> </ul> </div>