Software Model Checking via Summary-Guided Search
summary
GPS presents a concrete algorithm that interleaves directed testing with summary-guided search: it queries an SMT solver for models, uses a summary oracle implemented via compositional recurrence analysis to both prune infeasible suffixes and generate tests, and adds an refutation-complete instrumentation so it will eventually find an error if one exists. Implementation evaluates on 297 call-free C programs, outperforms top SV-COMP tools (CPAchecker, variabs, Symbiotic) in solved benchmarks and runtime, and publishes reproducible artifacts.
AI-written summary · about
chapters (9)
- 0:00GPS algorithm introduction
- 1:25GPS method intuition
- 3:51Summaries guide path exploration
- 7:21Implementing summary oracle
- 8:43GPS benchmark evaluation
- 10:49Comparison with state-of-the-art
- 11:54Key takeaways for researchers
- 12:36Summary and conclusion
- 12:57Q&A
related talks
28mBounded Model Checking of PLC ST Programs using Rewriting Modulo SMT
18mSemantic-Type-Guided Bug Finding
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
18mSMT2Test: From SMT Formulas to Effective Test Cases
21mValidating SMT Solvers for Correctness and Performance via Grammar-based Enumeration
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
25mStructure-guided Local Improvement for Maximum Satisfiability
34mAbstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)