Efficient Summary Reuse for Software Regression Verification

Fei He, Qianshan Yu

Abstract

Software systems evolve throughout their life cycles. Many revisions are produced over time. Verifying each revision of the software is impractical. Regression verification suggests reusing intermediate results from the previous verification runs. This paper studies regression verification via summary reuse. Not only procedure summaries, but also loop summaries are proposed to be reused. This paper proposes a fully automatic regression verification technique in the context of CEGAR. A lazy counterexample analysis technique is developed to improve the efficiency of summary reuse. We performed extensive experiments on two large sets of industrial programs (3,675 revisions of 488 Linux kernel device drivers). Results show that our summary reuse technique saves 84% to 93% analysis time of the regression verification.

Artifact

TODO

Full Results

The full experimental results can be found in the following links:

Benchmark

The artificial benchmarks and real-world benchmarks can be found in the following link:

Reference

[1] D. Beyer, S. Lowe, E. Novikov, A. Stahlbauer, and P. Wendler, “Precision reuse for efficient regression verification,” in Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 2013, pp. 389–399.