Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: Efficient Implementation of Property Directed Reachability</h1> <div class='date'><time class="dtstart dt-start" title="2012-02-06T10:00:00" datetime="2012-02-06T10:00:00">Monday, February 6, 2012 from 10</time>–<time class="dtend dt-end" title="2012-02-06T11:00:00" datetime="2012-02-06T11: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>Presented by Alan Mishchenko.</p> <p>Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://corp.galois.com/blog/2012/1/31/tech-talk-efficient-implementation-of-property-directed-reac.html">Website</a></li> </ul> </div>