« Cloud Security Risk Agreements for Small Businesses | Main | Tech Talks: Back-to-back Talks on Haskell and Embedded Systems »
Friday
Aug192011

Tech Talk: Modular verification of preemptive OS kernels

Galois is pleased to announce the following tech talk.
These talks are open to the interested public. 

speaker:
Alexey Gotsman
IMDEA Software Institute, Madrid, Spain

time:
23 August 2011, 10:30 A.M.

location:
Galois, Inc.
421 SW 6th Ave.
Ste 300
Portland, OR 97007
(3rd floor of the Commonwealth Building) 

abstract:
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).

bio:
Alexey Gotsman is an Assistant Research Professor at the IMDEA Software Institute in Madrid, Spain. Before joining IMDEA, he was a postdoctoral fellow at the University of Cambridge, where he also obtained his Ph.D. His research interests are in software verification, particularly, in developing reasoning techniques and automated verification tools for real-world concurrent system software.

Alexey Gotsman is an Assistant Research Professor at the IMDEA Software Institute in Madrid, Spain. Before joining IMDEA, he was a postdoctoral fellow at the University of Cambridge, where he also obtained his Ph.D. His research interests are in software verification, particularly, in developing reasoning techniques and automated verification tools for real-world concurrent system software.

 

Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Post:
 
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>