Source-linked AI summary
CPAchecker: A Tool for Configurable Software Verification
Dirk Beyer, M. Erkan Keremoglu
TL;DR
Software-verification approaches are difficult to compare and extend because implementations entangle analysis components and experimental environments. CPAchecker addresses this with a CPA-based framework whose generic reachability algorithm composes interchangeable analyses and interfaces. Initial experiments on verification benchmarks were reported as satisfactory, under specified hardware, memory, and time limits.
Problem
Software-verification approaches are difficult to compare because implementation choices such as parsers, theorem provers, and pointer-alias analyses affect performance and precision.
Method
CPAchecker transforms programs into control-flow automata and applies a generic reachability algorithm to CPAs and their configurable compositions.
Results
The initial CPAchecker experiments achieved satisfactory overall performance while prioritizing a portable and flexible environment over optimization.
Takeaways & Limitations
CPAchecker provides an extensible framework for integrating verification techniques and comparing them in a common experimental setting.
Takeaways & Limitations
The experiments were conducted with a 1.8 GB Java virtual-machine memory limit and a 1200 s termination time limit.
Abstract
from arXiv · showhide
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, 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. We evaluate the efficiency of our tool on benchmarks from the software model checker BLAST. The first released version of CPAchecker implements CPAs for predicate abstraction, octagon, and explicit-value domains. Binaries and the source code of CPAchecker are publicly available as free software.
(Tool Paper)
The paper is authored by Dirk Beyer and M. Erkan Keremoglu, with an affiliation at Simon Fraser University in British Columbia, Canada.
- Dirk Beyer and M. Erkan Keremoglu are listed as the authors.
- The authors are affiliated with Simon Fraser University, B.C., Canada.
- The listed institutional location is British Columbia, Canada.
1 Overview
CPAchecker addresses the difficulty of comparing software-verification approaches by providing a configurable framework based on a common CPA formalism. Its open-source implementation is intended to support reproducible experimentation and integration of new verification techniques.
- Software-verification research advances rapidly, but evaluating new approaches requires substantial infrastructure engineering.Examples include parser-front-end adaptation, syntax-tree transformation, and theorem-prover interaction.
- Different tools are difficult to compare because parser, theorem-prover, and pointer-alias-analysis choices affect performance and precision.These environmental differences make component-level performance comparisons difficult.
- CPA provides a common formal setting and interface for expressing program analyses through abstract-domain, post, merge, and stop operators.
- CPAchecker implements loosely dependent, substitutable components so different approaches can be compared in the same experimental setting.The paper states that this makes experimental results more meaningful or valid.
- CPAchecker is presented as an open-source, free-software platform intended to help researchers integrate verification techniques and improve practitioner access.
2 Architecture and Implementation
CPAchecker translates programs into control-flow automata and applies a generic reachability algorithm to configurable CPA combinations. Its interface-based architecture supports adding domains, composing analyses, and varying operators for experiments.
- Architecture: Input programs are parsed into syntax trees and then transformed into control-flow automata containing locations and operation edges.Edges represent assume operations, assignment blocks, function calls, or function returns.
- Implementation: CPAchecker provides interfaces to SMT solvers, interpolation procedures, BDDs, and octagon representations.
- Architecture: The central algorithm performs reachability analysis through the CPA interface without depending on a particular concrete CPA.Most configurations use a composite CPA that combines several CPAs.
- Design for extension: Adding a new abstract domain requires registering the CPA in the global properties file and implementing the CPA and its operation interfaces.
- Design for extension: Its extension design separates abstract CPA interfaces from implementations such as Composite CPA and User CPA.Different merge-operator implementations can be configured for experiments.
3 Experiments
The experiments evaluate CPAchecker on simplified Windows device-driver safety problems using combined explicit-value and predicate-abstraction analyses. Results indicate satisfactory performance, with threshold 5 providing the best overall tradeoff and explicit values reducing predicate-abstraction effort.
- Experimental setup: The evaluation combines explicit-value analysis with predicate abstraction on safety verification problems for simplified Windows device drivers.The experiments use a previously established configuration and examine reachability of error locations under variable-value conditions.
- Overall assessment: CPAchecker’s initial performance results are satisfactory, although the design prioritizes portability and flexibility over optimization.The experiments ran on GNU/Linux with a 1.8 GB Java memory limit and a 1200-second termination limit.
- Experimental setup: Table 1 reports processor-time runtimes across five explicit-value thresholds for the combined analysis configuration.The thresholds specify how many explicit values are tracked per variable; 0 denotes pure predicate abstraction and ∞ pure explicit-value analysis.
- Performance results: Threshold 5 achieves the best total performance for this set of programs, balancing predicate abstraction against the potentially exploding explicit-value analysis.Pure predicate abstraction times out on some experiments, while threshold 5 is reported as the best overall tradeoff.
- Analysis behavior: Explicit-value tracking drastically reduces predicates in abstract-successor computations and significantly reduces the refinement iterations needed to obtain verification results.Table 2 records predicate counts and refinement steps; a dash indicates an experiment aborted after 20 minutes.