Variance analyses from invariance analyses
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.
Speaker Details
Dr. Byron Cook is researcher at Microsoft’s laboratory at Cambridge University. He is also a visiting professor at Chalmers University and at Queen Mary, University of London. Byron’s research interests include automatic formal software verification, automatic theorem proving, and programming language theory. Byron has recently been working on automatic tools for proving program termination and tools for proving properties about data structures. Byron is one of the developers behind the SLAM software model checker. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers. Before joining Microsoft, Byron worked at Prover Technology, where he investigated new algorithms for use in SAT solvers and symbolic model checking tools. Byron’s PhD is from OGI.For more information about Dr. Cook, see http://research.microsoft.com/~bycook
- Date:
- Speakers:
- Byron Cook
- Affiliation:
- Microsoft Research Cambridge
-
-
Byron Cook
-
Jeff Running
-
