Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois tech talk: Effective Verification of Low-Level Software with Nested Interrupts</h1> <div class='date'><time class="dtstart dt-start" title="2015-07-28T11:00:00" datetime="2015-07-28T11:00:00">Tuesday, July 28, 2015 from 11am</time>–<time class="dtend dt-end" title="2015-07-28T12:00:00" datetime="2015-07-28T12:00:00">noon</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202394717'><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 Ste 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%20Ste%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>abstract:</p> <p>Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads. We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional formal approaches that use source-to-source transformations.Our experimental results show that our method significantly outperforms conventional techniques. To the best of our knowledge, our technique is the first to demonstrate effective formal verification of low-level embedded software with nested interrupts.</p> <p>bio:</p> <p>Lihao Liang is a PhD student in the Department of Computer Science of University of Oxford, working with Daniel Kroening, Tom Melham and Luke Ong. His research is supported by an Intel funded project Effective Validation of Firmware. He is interested in automated software analysis and verification, particularly concurrent software and synchronization primitives such as read-copy update (RCU).</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://galois.com/blog/2015/07/tech-talk-effective-verification-low-level-software-nested-interrupts/">Website</a></li> </ul> </div>