BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:DAYLIGHT
DTSTART:20110313T020000
RDATE:20110313T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110819T221826Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110823T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110823T103000
DTSTAMP;VALUE=DATE-TIME:20110819T221826Z
LAST-MODIFIED;VALUE=DATE-TIME:20110822T142933Z
UID:http://calagator.org/events/1250461233
DESCRIPTION:Presented by Alexey Gotsman\n\nMost major OS kernels today ru
 n on multiprocessor systems and are preemptive: it is possible for a pro
 cess running in the kernel mode to get descheduled. Existing modular tec
 hniques for verifying concurrent code are not directly applicable in thi
 s 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\, w
 here the scheduler and processes interact in complex ways. In this talk 
 I will present  the first logic that is able to decompose the verificati
 on 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 kern
 els. This is joint work with Hongseok Yang (University of Oxford\, UK).\
 n\nTags: tech talk\, galois\, formal methods\n\nImported from: http://ca
 lagator.org/events/1250461233
URL:https://corp.galois.com/blog/2011/8/19/tech-talk-modular-verification
 -of-preemptive-os-kernels.html
SUMMARY:Tech Talk: Modular verification of preemptive OS kernels
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:2
END:VEVENT
END:VCALENDAR