PV3 ⊧ CPACheckerchecks user-specified assertions in C programSoftware verification framework
- Software verification
- Model checking
- Software model checking
Type of toolModel checker?
- C program
- CPAChecker will look for labels named
ERROR(case insensitive) and assertions in the source code file
- Configuration file (there are default configurations available) which indicates what kind of analysis to perform
- C program:
UNKNOWN which indicates whether it found a violation of the property/assertion in the program.
HTML report named
Report.html if the result was
Counterexample.*.html if the result was
FALSE. You can open these HTML files in a browser to view the analysis results.
The results include things such as a visualization of the control flow, counterexample (if there was an error) and time statistics.
InternalsSome techniques that are implemented/available in CPAChecker include:
- Predicate abstraction
- Interpolation-based refinement
- Adjustable-block encoding