CPAchecker with Adjustable Predicate Analysis (Competition Contribution)

摘要

CPACHECKER is a freely available software-verification framework, built on the concepts of Configurable Program Analysis (CPA). CPAchecker integrates most of the state-of-the-art technologies for software model checking, such as counterexample-guided abstraction refinement (CEGAR), lazy predicate abstraction, interpolation-based refinement, and large-block encoding. The CPA for predicate analysis with adjustable-block encoding (ABE) is very promising in many categories, and thus, we submit a CPAchecker configuration that uses this analysis approach to the competition.