Incremental Predicate Analysis for Regression Verification
summary
Implements an end-to-end regression-verification pipeline on CPAchecker that reuses assertion annotations across revisions: a CFA Diff based on similarity flooding finds changed edges and location mappings, a forward-slicing change-impact analysis computes impacted variables, a reuse-annotation step weakens assertions conservatively, and an incremental predicate analysis initializes with those annotations and runs predicate analysis. Evaluated on 1,119 revisions of 62 Linux drivers (4,193 tasks), it achieves 2.8x speedup, solves 393 additional tasks, uses fewer abstract states and less memory.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:21Problem
- 3:04Predicate Analysis as Assertion Annotation
- 3:37Motivation
- 4:13Our Approach
- 6:43CFA Diff
- 8:27Change Impact Analysis
- 10:54Reuse Annotation
- 13:26Evaluation
- 15:29Conclusion
related talks
01h 00mContinuous Regression Testing for Safer and Faster Refactoring in C++
18mPreview: Verification (Correctness & Debugging)
18mPreview: Verification (Correctness)
23mBeyond Tests What to Verify in AI Generated Code
15mEvaluating Soundness of a Gradual Verifier with Property Based Testing
18mAn Efficient Runtime Validation Framework based on the Theory of Refinement
21mCombined Dynamic and Formal Verification Approach to Processor Verification
23mStop Performance Regressions Before Release Valkey’s CI Benchmarking