Comparison between CPBPV, ESC/Java, CBMC, Blast, EUREKA and Why for Bounded Program Verification
H\'el\`ene Collavizza (I3S), Michel Rueher (I3S), Pascal Van, Hentenryck (Brown University)
TL;DR
This paper compares the effectiveness of several program verification tools, including CPBPV, ESC/Java, CBMC, Blast, EUREKA, and Why, using a set of benchmark programs to evaluate their capabilities.
Contribution
It provides an experimental comparison of multiple bounded program verification frameworks on benchmark tests, highlighting their relative strengths and limitations.
Findings
CPBPV shows competitive performance on benchmarks
Different tools excel in different verification scenarios
The study offers insights into tool selection for bounded program verification
Abstract
This report describes experimental results for a set of benchmarks on program verification. It compares the capabilities of CPBVP "Constraint Programming framework for Bounded Program Verification" [4] with the following frameworks: ESC/Java, CBMC, Blast, EUREKA and Why.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Parallel Computing and Optimization Techniques