Software Verification with CPAchecker 3.0: Tutorial and User Guide
Daniel M Baier, Dirk Beyer, Po-Chun Chien, Marie-Christine Jakobs, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas R. Lemberger, Marian Lingsch-Rosenfeld, Henrik Wachowitz, Philipp Wendler · Lecture notes in computer science · 2024
Abstract This tutorial provides an introduction toCPAcheckerfor users.CPAcheckeris a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking,Impact, interpolation-based model checking,k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases forCPAcheckerin formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases ofCPAcheckerfor test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge ofCPAcheckeris not required. This tutorial and user guide is based onCPAcheckerin version 3.0. This user guide’s latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php .