Incremental Verification of Compiler Optimizations

TitleIncremental Verification of Compiler Optimizations
Publication TypeConference Paper
Year of Publication2014
AuthorsFedyukovich, Grigory, Gurfinkel A., and Sharygina Natasha
Conference NameNASA Formal Methods (NFM)
Conference LocationHouston, Texas, USA
Abstract
Optimizations are widely used along the lifecycle of software. However, proving the equivalence between original and optimized versions is difficult. In this paper, we propose a technique to incrementally verify different versions of a program with respect to a fixed property. We exploit a safety proof of a program given by a safe inductive invariant. For each optimization, such invariants are adapted to be a valid safety proof of the optimized program (if possible). The cost of the adaptation depends on the impact of the optimization and is often less than an entire re-verification of the optimized program. We have developed a preliminary implementation of our technique in the context of Software Model Checking. Our evaluation of the technique on different classes of industrial programs and standard LLVM optimizations confirms that the optimized programs can be re-verified efficiently.
Full Text