Variance analyses from invariance analyses
Variance analyses from invariance analyses
复制标题
DOI：
10.1145/1190216.1190249
复制
发表时间：
2007-01
期刊：
影响因子：
--
通讯作者：
Josh Berdine;A. Chawdhary;B. Cook;Dino Distefano;P. O'Hearn
中科院分区：
文献类型：
--
作者：
Josh Berdine;A. Chawdhary;B. Cook;Dino Distefano;P. O'Hearn
对于程序位置l的不变性断言是在程序执行期间始终在l处保持的语句。程序不变性分析推断不变性断言，这在试图证明安全属性时可能很有用。我们使用术语方差断言来表示在l处的任何状态和也在l处的任何先前状态之间保持的语句。本文主要讨论方差断言分析的发展及其在证明终止性和活性性质中的应用。我们描述了一种从不变性分析构造程序方差分析的方法。如果我们改变基本的不变性分析，我们会得到不同的方差分析。我们描述了几个应用的方法，包括方差分析，使用线性算术和形状分析。使用实验结果，我们表明，这些方差分析产生了一个新的品种的终止证明竞争力，有时比今天的国家的最先进的终止证明。
An invariance assertion for a program location l is a statement that always holds at l 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 statement that holds between any state at l and any previous state that was also at l. This paper is concerned with 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.