CPAchecker is a framework for software verification, built on the foundations of Configurable Program Analysis (CPA). For the SV-COMP'14, we file a CPAchecker configuration that runs up to five analyses in sequence. The first two analyses of our approach utilize the explicit-value domain for modeling the state space, while the remaining analyses are based on predicate abstraction. In addition to that, a bit-precise counterexample checker comes into action whenever an analysis finds a counterexample. The combination of conceptually different analyses is key to the success of our verification approach, as the diversity of verification tasks is taken into account. © 2014 Springer-Verlag.
CITATION STYLE
Löwe, S., Mandrykin, M., & Wendler, P. (2014). CPAchecker with sequential combination of explicit-value analyses and predicate analyses (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8413 LNCS, pp. 392–394). Springer Verlag. https://doi.org/10.1007/978-3-642-54862-8_27
Mendeley helps you to discover research relevant for your work.