PV3 ⊧ CPACheckerchecks user-specified assertions in C program

Software verification framework

Application domain/field

• Software verification
• Model checking
• Software model checking

Type of tool

Model checker?

Expected input

• 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

Format:

• C program: .c file
• Configuration: .properties file

Expected output

Verification result: FALSE or TRUE or UNKNOWN which indicates whether it found a violation of the property/assertion in the program. HTML report named Report.html if the result was TRUE or 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.

Internals

Some techniques that are implemented/available in CPAChecker include:

• Predicate abstraction
• Interpolation-based refinement
• Adjustable-block encoding

Uses MathSAT, CSIsat, CBMC, JavaBDD.

Comments

License: Apache 2.0 License