CPAchecker: A Tool for Configurable Software Verification

Download Now Free registration required

Executive Summary

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 paper 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.

  • Format: PDF
  • Size: 264.12 KB