Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
"Proving that software eventually does something good"
Byron Cook
Microsoft Research
SWS Distinguished Lecture Series - Spring
Dr. Byron Cook is researcher at Microsoft's laboratory at Cambridge University. His research interests include topics in program verification, theorem proving, and programming languages. In recent years Byron has been working on program termination, shape analysis, and software model checking. Byron is one of the developers behind the SLAM software model checker and the SLAM-based Windows product called Static Driver Verifier, which attempts to automatically prove the correctness of Windows OS device drivers with respect to a fixed set of safety properties.
 |
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 16 May 2008
16:00
60 Minutes
Fraunhofer-Zentrum
Auditorium
Kaiserslautern
Abstract
Recent research advances now allow us to automatically prove termination and other liveness properties of programs. In cases where the desired property does not hold for all inputs, tools can be used to synthesize a precondition on the inputs under which the property does hold. In this talk I will describe these recent advances and discuss our efforts to apply termination analysis to the problem of proving that device drivers do not hang the Windows operating system.
Contact
Brigitta Hansen
0681 - 9325200
--email hidden
Video Broadcast
Yes
MPI-SWS Saarbrücken
E 1 4
Raum 019
passcode not visible
logged in users only
Carina Schmitt, 05/26/2008 14:24
Brigitta Hansen, 05/13/2008 17:37
Brigitta Hansen, 05/08/2008 11:36 -- Created document.
Brigitta Hansen, 05/13/2008 17:37
Brigitta Hansen, 05/08/2008 11:36 -- Created document.