sosylab/cpachecker repository overview

⁠CPAchecker⁠⁠, the Configurable Software-Verification Platform

This is a Docker image for CPAchecker, the Configurable Software-Verification Platform⁠.

⁠Quick reference

• Maintained by: SoSy-Lab @ LMU Munich⁠
• Where to get help: Documentation⁠, Issue Tracker⁠, Mailing Lists⁠

⁠Supported tags and respective Dockerfile

• latest⁠: latest release version of CPAchecker⁠
• dev⁠: latest development version of CPAchecker⁠
• {version}⁠: specific release version of CPAchecker. Only the image of the latest version of CPAchecker gets regularly updated, older versions do not get updated once a later version is available.

⁠What is CPAchecker?

CPAchecker is a tool for configurable software verification. The implementation is based on the concepts described in the CAV'07 paper "Configurable Software Verification"⁠ and in the ASE'08 paper "Program Analysis with Dynamic Precision Adjustment"⁠. The basic architecture of CPAchecker is explained in the CAV'11 paper "CPAchecker: A Tool for Configurable Software Verification"⁠.

A list of many more publications related to CPAchecker is available on our web page⁠.

CPAchecker is used to verify Linux kernel drivers by the Linux Driver Verification project⁠ and Klever⁠, and hundreds of bugs in Linux have already been found with CPAchecker and fixed consequently (cf. list of fixes for bugs found with CPAchecker⁠).

⁠How to use this image

Run the below command to pull and run the latest CPAchecker version through docker:

docker run sosylab/cpachecker /cpachecker/doc/examples/example.c

This command runs CPAchecker in its default configuration on an example file that is shipped with CPAchecker.

More information about command-line parameters to CPAchecker are available in the CPAchecker documentation⁠.

⁠Output files

CPAchecker produces a number of output files. To save these files to the host system, mount your current working directory to the /workdir directory in the container and use the -u option to run CPAchecker with the same user ID and group ID as the host user:

docker run \
    -v $(pwd):/workdir \
    -u $UID:$GID \
    sosylab/cpachecker /cpachecker/doc/examples/example.c

CPAchecker stores output files in directory output/.

⁠Analyzing arbitrary programs

To analyze a program that is not shipped with CPAchecker, mount the directory that contains the program and adjust your command-line to point to that program file.

⁠Image details

dev⁠ images are built regularly from the latest commit in the CPAchecker repository's⁠ default branch. They are based on ubuntu:latest⁠.

latest⁠ images are built regularly from the latest release version of CPAchecker. They are based on ubuntu:20.04⁠

⁠License

CPAchecker is licensed under the Apache 2.0 License⁠ with copyright by Dirk Beyer⁠.

Third-party libraries are under various other licenses and copyrights. See the full license texts⁠ for more details. In particular, MathSAT is available for research and evaluation purposes only⁠, so make sure to use a different SMT solver if necessary. Note that although a GPL program is distributed together with CPAchecker, CPAchecker is separate from that program and thus not under the terms of the GPL.

Our docker images also contain other software which may be under other licenses, such as Bash and other software from the base distribution, along with any dependencies that may be installed in the process of building the image.

⁠Alternative Sources

A mirror of this image is available as registry.gitlab.com/sosy-lab/software/cpachecker⁠⁠.
CPAchecker releases are permanently archived at Zenodo⁠.