When Regression Verification Meets CEGAR

TL;DR

This paper introduces an automatic regression verification method combining CEGAR and procedure summaries, enabling efficient reuse across program revisions and abstract precisions, significantly improving verification performance.

Contribution

It proposes using procedure summaries as reusable intermediate results in CEGAR-based regression verification, enhancing efficiency across software revisions.

Findings

Significant performance improvements on industrial Linux kernel driver revisions.

Procedure summaries are small, easy to process, and require minimal extra computation.

The approach effectively reuses information across different program versions and analysis precisions.

Abstract

Software systems evolve throughout their life cycles. Many revisions are produced over time. Model checking each revision of the software is impractical. Regression verification suggests reusing intermediate results from the previous verification runs. This paper proposes a fully automatic regression verification technique in the context of CEGAR. Procedure summaries, which describe the input/output behaviors of a procedure, are proposed as the intermediate results to be reused. Procedure summaries are reasonably small to store, technically easy to process, and do not require much extra computation effort to be reused. Reusing procedure summaries saves much analysis effort on the corresponding procedures. By combining regression verification and CEGAR, we propose a technique that is able to reuse procedure summaries across different abstract precisions and different program revisions. We performed extensive experiments on a large number of industrial programs (534 revisions of 89 Linux kernel device drivers). The results show that our approach can significantly improve the performance of regression verification.