CPAchecker: A Software Verification Tool for Configurable Program Analyses

CPAchecker: A Tool for Configurable Software Verification

Software Systems Lab
University of Passau, Bavaria, Germany

Objectives

Configurable Verification Plattform

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 and Erkan Keremoglu

Download

CPAchecker is free software (Apache 2.0 License)
Current version 0.9: Check out from repository (or browse through).
Supplementary web page of our paper about Large-Block Encoding.

SVN repository: http://svn.sosy-lab.org/software/cpachecker (currently, you still need to request an account first)
Project page available at Google Code: http://cpachecker.googlecode.com (not yet active)
(includes source-code repository and downloads).

Mailing Lists

We provide mailing list for differents 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 HowToMailing.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).

Documentation

Configurable Software Verification. CAV 2007
Program Analysis with Dynamic Precision Adjustment. ASE 2008
Tutorial coming soon
Browse through the source code

Papers based on CPAchecker

Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A Tool for Configurable Software Verification. Technical report SFU-CS-2009-02, School of Computing Science (CMPT), Simon Fraser University (SFU), January 2009.
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.

Acknowledgements

We thank the following people for their help:

Gregor Endler, University of Passau, Germany
Alberto Griggio, University of Trento, Italy
Tom Henzinger, IST Austria, Austria
Andreas Holzer, Technical University of Darmstadt, Germany
Michael Käufl, University of Passau, Germany
Michael Tautschnig, Technical University of Darmstadt, Germany
Gregory Theoduloz, EPFL, Switzerland
Philipp Wendler, University of Passau, Germany

(A complete and detailed list can be found in the file Authors.txt in the project trunk.)

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

Last updated: $Date: 2010-02-06 11:38:39 +0100 (Sat, 06 Feb 2010) $ by $Author: dbeyer $