Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Variance analyses from invariance analyses

Speaker  Byron Cook

Affiliation  Microsoft Research Cambridge

Host  Shuvendu Lahiri

Duration  00:59:22

Date recorded  8 August 2006

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.

©2006 Microsoft Corporation. All rights reserved.
> Variance analyses from invariance analyses