CPAchecker: A Software Verification Tool for Configurable Program Analyses

Objectives

Configurable Verification Platform
CPAchecker is a tool for configurable software verification. Our implementation is guided by the concepts described in the CAV'07 paper "Configurable Software Verification" and in the ASE'08 paper "Program Analysis with Dynamic Precision Adjustment".

The name CPAchecker was chosen to reflect that the tool is based on the CPA concepts and is used for checking software programs.

Authors/Maintainers: Dirk Beyer, Stefan Löwe, and Philipp Wendler

Documentation

Instructions for installation
If you have problems with the installation, please contact us (either via mailing list or Dirk).
Getting started with CPAchecker
More information ...
Tutorial coming soon
Browse through the source code

Configurable Software Verification. CAV 2007
Program Analysis with Dynamic Precision Adjustment. ASE 2008
Predicate Abstraction with Adjustable-Block Encoding. FMCAD 2010

Papers based on CPAchecker

Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011, Snowbird, UT, July 14-20), LNCS 6806, pages 184-190, 2011. Springer-Verlag, Berlin.
Dirk Beyer, M. Erkan Keremoglu, and Philipp Wendler. Predicate Abstraction with Adjustable-Block Encoding. In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010, Lugano, October 20 - 23), 2010. Supplementary web page.
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, and Roberto Sebastiani. Software Model Checking via Large-Block Encoding. In Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009, Austin (TX), November 15-18), 2009. IEEE Computer Society Press, Los Alamitos (CA). Supplementary web page.

Mailing Lists

We provide mailing lists for different audiences (cpachecker-announce, cpachecker-users, cpachecker-commits, cpachecker-dev).
A description of the mailing lists and how to subscribe can be found in the file Mailing.txt in the project trunk.
For installation questions, bug reports, and suggestions, please send email to CPAchecker-Users (the domain is always sosy-lab.org).

Download / Installation

CPAchecker is free software (Apache 2.0 License)

Download lasted binary release: CPAchecker-1.1-unix.tar.bz2 and CPAchecker-1.1-windows.zip
Check out sources from SVN repository: https://svn.sosy-lab.org/software/cpachecker/trunk
SVN mirror available at Google Code: http://cpachecker.googlecode.com (read-only check-out)
Trac web site: http://cpachecker.sosy-lab.org/trac (same account as for SVN access)
Browse through the current trunk version
Supplementary web page of our paper about Large-Block Encoding
Supplementary web page of our paper about Adjustable-Block Encoding

Build-Bot (regression tests on example programs and verification benchmarks)
Just for Fun: Visualization of CPAchecker Project History

News: (Full list: https://svn.sosy-lab.org/software/cpachecker/trunk/NEWS.txt)

Changes since CPAchecker 1.1
----------------------------
* r5060: A time limit of 15 minutes is now enabled by default in most configurations.
  If the analysis is not yet finished, CPAchecker will stop after this time and report UNKNOWN.
  The time limit can be controlled with the "cpa.conditions.global.time.wall" option
  and the "-timelimit" command-line argument.
  Example:
  scripts/cpa.sh -predicateAnalysis -timelimit 1min test.c
* r4960: If the #include directive of specification automata is used with relative paths, 
  the base directory of the relative path is now the directory of the file which contains the #include,
...

Acknowledgements

We thank the following people for their help: (Source: https://svn.sosy-lab.org/software/cpachecker/trunk/Authors.txt)

Main Authors/Maintainers:
  Dirk Beyer (since 2007), Simon Fraser University, Canada / University of Passau, Germany
  Stefan Löwe (since 2010), University of Passau, Germany
  Philipp Wendler (since 2009), University of Passau, Germany

Former Maintainers:
  Erkan Keremoglu (2008 - 2011), Simon Fraser University, Canada

Contributors:
  Gregor Endler (2009 - 2010), University of Passau, Germany
  Karlheinz Friedberger (2011), University of Passau, Germany
  Alberto Griggio (2008 - 2009), Simon Fraser University, Canada / University of Trento, Italy
  Peter Häring (2011), University of Passau, Germany
  Andreas Holzer (2008 - 2011), University of Darmstadt, Germany / TU Vienna, Austria
  Michael Käufl (2011), University of Passau, Germany
  Steven Kieffer (2011), Simon Fraser University, Canada
  Alexander von Rhein (2010), University of Passau, Germany
  Andreas Stahlbauer (2011), University of Passau, Germany
  Michael Tautschnig (2008 - 2009), University of Darmstadt, Germany
  Gregory Theoduloz (2009 - 2010), EPFL, Switzerland
  Daniel Wonisch (2011), University of Paderborn, Germany
  Geoff Zenger (2007), Simon Fraser University, Canada

Questions and bug reports:
  Dirk Beyer: CPAchecker-Users@sosy-lab.org

Friends of CPAchecker

The following projects use CPAchecker's technology, or perform research on related technology:

BLAST: A Software Model Checker for C
Predecessor of CPAchecker, BLAST was proving useful many ideas that we integrated in CPAchecker as well.
CSIsat and MathSAT: Interpolating SMT solvers for LA+EUF
CPAchecker uses CSIsat and MathSAT for solving interpolation and satisfiability queries.
Jakstab: A Static Analysis Platform for Binaries
Implementation based on Configurable Program Analysis.
LDV: Linux Driver Verification
Research group that verifies Linux drivers using CPAchecker.
SyCMC: A Software Model Checker for System-C
Implementation based on Large Block Encoding.

Author: Dirk Beyer, other project pages: BLAST, CCVisu, Chic, CrocoPat, CSIsat, Rabbit

Last updated: $Date: 2011-12-21 15:19:44 +0100 (Wed, 21 Dec 2011) $ by $Author: dbeyer $

CPAchecker

A Tool for Configurable Software Verification