Abstract
We submit to SV-COMP’15 the software-verification framework CPAchecker. The submitted configuration is a combination of seven different analyses, based on explicit-value analysis, k-induction, predicate analysis, and concrete memory graphs. These analyses use concepts such as CEGAR, lazy abstraction, interpolation, adjustableblock encoding, bounded model checking, invariant generation, and blockabstraction memoization. Found counterexamples are cross-checked by a bit-precise analysis. The combination of several different analyses copes well with the diversity of the verification tasks in SV-COMP.
Cite
CITATION STYLE
Dangl, M., Löwe, S., & Wendler, P. (2015). CPACHECKER with support for recursive programs and floating-point arithmetic (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9035, pp. 423–425). Springer Verlag. https://doi.org/10.1007/978-3-662-46681-0_34
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
