CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution).

CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution).

Авторы

S. Löwe, M. Mandrykin, P. Wendler.

Аннотация

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 (на английском)

Ключевые слова

competition on software verificaition, software verification tool, sequential combination of analyses

Издание

Proceedings of TACAS. 2014. pp. 392-394.

DOI: 10.1007/978-3-642-54862-8_27

Научная группа

Технологии программирования

Все публикации за 2014 год Все публикации