Byron Cook

(Microsoft Research, Cambridge)

"Proving that software eventually does something good"

(Vortrag im Rahmen der "Distinguished Lecture Series Spring 2008" des Max Planck Instituts für Software-Systeme)

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.

Zeit:	Freitag, 16. Mai 2008, 16:00 Uhr
Ort:	Fraunhofer-Zentrum Kaiserslautern, Auditorium
Hinweis:	Der Vortrag wird live an die Universität des Saarlandes MPI-Gebäude E1.4 Raum 019 übertragen.