When Regression Verification Meets CEGAR
This work addresses the challenge of efficient model checking for software revisions, offering a domain-specific incremental improvement for verification in software engineering.
The paper tackles the problem of verifying evolving software systems by proposing a fully automatic regression verification technique that reuses procedure summaries across different abstract precisions and program revisions, resulting in significant performance improvements as demonstrated on 534 revisions of 89 Linux kernel device drivers.
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.