Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Tech Talk: Modular verification of preemptive OS kernels</h1> <div class='date'><time class="dtstart dt-start" title="2011-08-23T10:30:00" datetime="2011-08-23T10:30:00">Tuesday, August 23, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-08-23T11:30:00" datetime="2011-08-23T11: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 Alexey Gotsman</p> <p>Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU, where the scheduler and processes interact in complex ways. In this talk I will present the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components present in mainstream kernels. This is joint work with Hongseok Yang (University of Oxford, UK).</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="https://corp.galois.com/blog/2011/8/19/tech-talk-modular-verification-of-preemptive-os-kernels.html">Website</a></li> </ul> </div>