CPAchecker: A Tool for Configurable Software Verification

Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism.  This talk explains CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, is required to implement the interface of configurable program analysis (CPA).

The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs.  The major design goal during the development was to provide a framework for developers that is flexible and easy to extend.  We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this platform and that it advances the field by making it easier to perform practical experiments. The tool is implemented in Java and runs as command-line tool or as Eclipse plug-in. CPAchecker is the proposed successor of well-known model checker BLAST, and is licensed as free software.