CPAchecker: A Tool for Configurable Software Verification

By Dirk Beyer, M. Erkan Keremoglu. International Conference on Computer Aided Verification, 2009

623 citations recorded by the source corpus.

Configurable software verification is a recent concept for expressing different program analysis and model checking approaches in one single formalism. This paper presents CPAchecker, a tool and framework that aims at easy integration of new verification components. Every abstract domain, together with the corresponding operations, implements the interface of configurable program analysis (CPA). The main algorithm is configurable to perform a reachability analysis on arbitrary combinations of existing CPAs. In software verification, it takes a considerable amount of effort to convert a verification idea into actual experimental results -- we aim at accelerating this process. We hope that researchers find it convenient and productive to implement new verification ideas and algorithms using this flexible and easy-to-extend 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 implements CPAs for several abstract domains. We evaluate the efficiency of the current version of our tool on software-verification benchmarks from the literature, and compare it with other state-of-the-art model checkers. CPAchecker is an open-source toolkit and publicly available.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/fa817a9520a9d2f12b04c770c9f5b26754c0d2ca

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Software

Citations in the corpus

The SeaHorn Verification Framework (2015, methodology): “The Control Flow category, was won by CPAChecker [9] getting 74% of the maximum score, while SeaHorn got 69%.”
A Classification and Survey of Analysis Strategies for Software Product Lines (2014, methodology): “NUSMV [Cimatti et al. 1999]), while others extract models directly from source code (e.g., C in BLAST [Beyer et al. 2007] or CPACHECKER [Beyer and Keremoglu 2011], Java in JPF[Visser et al. 2000]).”
Proving differential privacy with shadow execution (2019, methodology): “ ϵ ≤ϵ)never fails for any possible inputs that satisfy the precondition (i.e., the adjacency requirement). To demonstrate the usefulness of the transformed programs, we use a model checker CPAChecker [11] v1.8. CPAChecker is capable of automatically verifying C program with a given configuration. In”