PV3 CPACheckerchecks user-specified assertions in C program

Software verification framework

Application domain/field

Type of tool

Model checker?

Expected input


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.


Some techniques that are implemented/available in CPAChecker include: Uses MathSAT, CSIsat, CBMC, JavaBDD.


License: Apache 2.0 License


Related papers

Last publication date

November 2020

Related tools


ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.