CPAchecker is a freely available software-verification framework, built on the concepts of Configurable Program Analysis (CPA). Within CPAchecker, several such CPAs are available, e.g., a Predicate-CPA, building on the predicate domain, as well as an Explicit-CPA, in which an abstract state is represented as an explicit variable assignment. In the CPAchecker configuration we are submitting, the highly efficient Explicit-CPA, backed by interpolation-based counterexample-guided abstraction refinement, joins forces with an auxiliary Predicate-CPA in a setup utilizing dynamic precision adjustment. This combination constitutes a highly promising verification tool, and thus, we submit a configuration making use of this analysis approach. © 2013 Springer-Verlag.
CITATION STYLE
Löwe, S. (2013). CPAchecker with explicit-value analysis based on CEGAR and interpolation: (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7795 LNCS, pp. 610–612). https://doi.org/10.1007/978-3-642-36742-7_44
Mendeley helps you to discover research relevant for your work.