Description:
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(s):
Dr. Byron Cook, researcher, Microsoft's laboratory, Cambridge University
|
