Proving that Software eventually does something good

Byron Cook ( Microsoft Research )

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.

Bio: 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 Windows products 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. Before joining Microsoft, Byron worked at Prover Technology, where he investigated new algorithms for use in SAT solvers and symbolic model checking tools. Dr. Cook's PhD is from OGI.