BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Modular verification of preemptive OS kernels - Alexey Gotsman - I
 MDEA Software Institute
DTSTART:20111108T130000Z
DTEND:20111108T140000Z
UID:TALK33703@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION: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 cod
 e are not directly applicable in this setting: they rely on scheduling bei
 ng implemented correctly\, and in a preemptive kernel\, the correctness of
  the scheduler is interdependent with the correctness of the code it sched
 ules. This interdependency is even stronger in mainstream kernels\, such a
 s Linux\, FreeBSD or XNU\, where the scheduler and processes interact in c
 omplex ways. \n\nIn this talk I will present  the first logic that is able
  to decompose the verification of preemptive multiprocessor kernel code in
 to verifying the scheduler and the rest of the kernel separately\, even in
  the presence of complex interdependencies between the two components pres
 ent in mainstream kernels. \n\nThis is joint work with Hongseok Yang (Univ
 ersity of Oxford\, UK).\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR