CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution).
CPAchecker is a framework for software verication, built on the foundations of Configurable Program Analysis (CPA). For the SV-COMP'14, we file a CPAchecker conguration 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 verication approach, as the diversity of verication tasks is taken into account.Полный текст статьи в формате pdf (на английском)
Proceedings of TACAS. 2014. pp. 392-394.