Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois tech talk: Parallel K-induction based Model Checking</h1> <div class='date'><time class="dtstart dt-start" title="2011-07-12T10:30:00" datetime="2011-07-12T10:30:00">Tuesday, July 12, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-07-12T11:30:00" datetime="2011-07-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 Temesghen Kahsai.</p> <p>We give an overview of a parallel k-induction-based model checking architecture for verifying safety properties of synchronous systems. The architecture, which is strictly message-based, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic k-induction. A first level of parallelism is introduced in the k-induction procedure itself by executing the base and the inductive steps concurrently. A second level of parallelism allows the addition of one or more independent processes that incrementally generate invariants for the system being verified. The invariants are fed to the k-induction loop as soon as they are produced and used to strengthen the induction hypothesis.</p> <p>This architecture allows the verification of multiple properties in an incremental fashion. Specifically, the outcome of a property -- valid or invalid -- is communicated to the user as soon as the result is known. Moreover, verified valid properties are added as invariants in the model checking procedure to aid the verification of the remaining properties.</p> <p>We provide experimental evidence that this incremental and parallel architecture significantly speeds up the verification of safety properties. Additionally, due to the automatic invariant generation, it also considerably increases the number of provable safety properties.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://corp.galois.com/blog/2011/7/5/tech-talk-parallel-k-induction-based-model-checking.html">Website</a></li> </ul> </div>