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

Date, Time and Location

Friday, 16 May 2008
60 Minutes


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.


Brigitta Hansen
0681 - 9325200
--email hidden

Video Broadcast

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.