Advertisement
Published in:
2014 | OriginalPaper | Chapter
CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses
(Competition Contribution)
Authors : Stefan Löwe, Mikhail Mandrykin, Philipp Wendler
Published in: Tools and Algorithms for the Construction and Analysis of Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.