CPAchecker is a highly versatile framework for software verification of C programs. Its versatility is one reason for its yearly success in the international competetion on software verification (SV-COMP). CPAchecker is based on the established concept of configurable program analysis, which allows to implement abstract domains as individual CPAs and to freely combine them. Additionally, many common verification algorithms are implemented in CPAchecker, allowing CPAchecker to benefit from the strengths of induction, abstract interpretation, interpolation, lazy abstraction, and block-abstraction memoization.

Our poster presents the CPAchecker configuration CPA-Seq, which participated in SV-COMP’19. In SV-COMP’19, CPAchecker applies strategy selection to pick for each verification task the most promising configuration from a predefined set of configurations. To check tasks dealing with concurrency, memory safety, overflows, recursion, or termination, it uses single, dedicated configurations. For all other tasks, CPAchecker considers a small set of hand-picked program features to select one of three sequential combinations of bit-precise analyses.