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.