CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST. CPAchecker is based on the idea of configurable program analysis which is a concept that allows expression of both

model checking In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...

and program analysis with one formalism. When executed, CPAchecker performs a reachability analysis, i.e., it checks whether a certain state, which violates a given specification, can potentially be reached. One application of CPAchecker is the verification of

Linux Linux ( or ) is a family of open-source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically packaged as a Linux distribution, which ...

device driver In computing, a device driver is a computer program that operates or controls a particular type of device that is attached to a computer or automaton. A driver provides a software interface to hardware devices, enabling operating systems and ot ...

Achievements

CPAchecker came first in two categories (Overall and ControlFlowInteger) in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in

Tallinn Tallinn () is the most populous and capital city of Estonia. Situated on a bay in north Estonia, on the shore of the Gulf of Finland of the Baltic Sea, Tallinn has a population of 437,811 (as of 2022) and administratively lies in the Harju ' ...

. CPAchecker came first (category Overall) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in

Rome , established_title = Founded , established_date = 753 BC , founder = King Romulus (legendary) , image_map = Map of comune of Rome (metropolitan city of Capital Rome, region Lazio, Italy).svg , map_caption ...

Architecture

CPAchecker operates on a control-flow automaton (CFA); before a given C program can be analyzed by the CPA algorithm, it gets transformed into a CFA. A CFA is a directed graph whose edges represent either assumptions or assignments and its nodes represent program locations.

References

External links

* {{Official website, cpachecker.sosy-lab.org Java platform software C programming language family Formal methods tools Static program analysis tools Software testing tools Abstract interpretation