Title: Automatically Proving Concurrent Programs Correct
Speaker: Byron Cook
Place: Microsoft TechFest'07
Date: March 8th 2007
Materials: Video
Abstract: In this talk, I discuss several exciting new developments in the area of automatic tools for proving correctness properties of concurrent programs. This talk is aimed at a general audience.



Title: Variance Analyses from Invariance Analyses
Speaker: Byron Cook
Place: Microsoft Research, Redmond
Date: August 8th 2006
Materials: Video
Abstract: An invariance assertion for a program location "n" is a formula that always holds at "n" during execution of the program. Program invariance analyses infer invariance assertions that can be useful when trying to prove safety properties. We use the term "variance assertion" to mean a formula that holds between any state at "n" and any previous state that was also at "n". This talk will describe advances in the development of analyses for variance assertions and their application to proving termination and liveness properties. We describe a method of constructing program variance analyses from invariance analyses. If we change the underlying invariance analysis, we get a different variance analysis. We describe several applications of the method, including variance analyses using linear arithmetic and shape analysis. Using experimental results we demonstrate that these variance analyses give rise to a new breed of termination provers which are competitive with and sometimes better than today's state-of-the-art termination provers.



Title: Automatically proving the termination of C programs
Speaker: Byron Cook
Place: Isaac Newton Institute for Mathematical Sciences
Date: February 3rd 2006
Materials: slides and audio
Abstract: In this talk I will discuss Terminator, which is a program termination prover that supports large programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers. Terminator is based on a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. The termination argument is constructed incrementally, based on failed proof attempts. Terminator also infers and proves required program invariants on demand. The lecture will close with information about the results of some experiments with Terminator on Windows device drivers.



Title: Termination and shape-shifting heaps
Speaker: Byron Cook
Place: Isaac Newton Institute for Mathematical Sciences (During the Logic and Algorithms scientific programme).
Date: May 8th 2006
Materials: slides and audio
Abstract: This talk describes MUTANT/Terminator, a tool which is designed to prove termination of programs where the termination argument requires reasoning about the shape of the heap.