tag:calagator.org,2005:/events/searchCalagator: Events tagged with: model checking2016-05-02T11:09:43-07:00tag:calagator.org,2005:Calagator::Event/12504607982011-07-05T10:48:42-07:002011-07-05T10:48:42-07:00Galois tech talk: Parallel K-induction based Model CheckingTuesday, July 12, 2011 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504607982011-07-12T10:30:00-07:002011-07-12T11:30:00-07:00<div class="vevent">
<h1 class="summary">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">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='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>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" href="http://corp.galois.com/blog/2011/7/5/tech-talk-parallel-k-induction-based-model-checking.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/model checking">model checking</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250460798.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250460798/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, July 5, 2011 at 10:48am</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504619162012-01-31T17:57:30-08:002012-01-31T17:57:30-08:00Galois Tech Talk: Efficient Implementation of Property Directed ReachabilityMonday, February 6, 2012 from 10-11am at Galois, Inchttp://calagator.org/events/12504619162012-02-06T10:00:00-08:002012-02-06T11:00:00-08:00<div class="vevent">
<h1 class="summary">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">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='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>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" href="http://corp.galois.com/blog/2012/1/31/tech-talk-efficient-implementation-of-property-directed-reac.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/formal methods">formal methods</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/model checking">model checking</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250461916.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250461916/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Tuesday, January 31, 2012 at 5:57pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504702032016-05-02T11:09:43-07:002016-05-02T11:09:43-07:00Galois tech talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency.Wednesday, May 4, 2016 from 11am-noon at Galois Inchttp://calagator.org/events/12504702032016-05-04T11:00:00-07:002016-05-04T12:00:00-07:00<div class="vevent">
<h1 class="summary">Galois tech talk: Interrupts in OS code: let’s reason about them. Yes, this means concurrency.</h1>
<div class='date'><time class="dtstart dt-start" title="2016-05-04T11:00:00" datetime="2016-05-04T11:00:00">Wednesday, May 4, 2016 from 11am</time>–<time class="dtend dt-end" title="2016-05-04T12:00:00" datetime="2016-05-04T12:00:00">noon</time></div>
<div class="location vcard">
<a href='/venues/202394717' class='url'>
<span class='fn org'>Galois Inc</span>
</a>
<div class="adr">
<div class="street-address">421 Sw 6th Ave Ste 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20Sw%206th%20Ave%20Ste%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<h2>abstract:</h2>
<p>Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions.</p>
<p>In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task.</p>
<h2>bio:</h2>
<p>June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://galois.com/blog/2016/05/tech-talk-interrupts-in-os-code-lets-reason-about-them-yes-this-means-concurrency/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/Galois tech talk">Galois tech talk</a>, <a class="p-category" href="/events/tag/concurrency">concurrency</a>, <a class="p-category" href="/events/tag/model checking">model checking</a>, <a class="p-category" href="/events/tag/os">os</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250470203.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250470203/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Monday, May 2, 2016 at 11:09am</strong>.
</div>
</div>
</div>
45.5208 -122.6779