Reproduction Package for FM 2024 Article `Software Verification with CPAchecker: Tutorial and User Guide'

This package allows you to check the claims of our FM 2024 tutorial paperSoftware Verification with CPAchecker: Tutorial and User Guide. See the README.html for more information. Abstract:This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as predicates, explicit values, intervals, BDDs, and memory graphs, and many program-analyses and model-checking algorithms, such as symbolic execution, predicate abstraction, bounded model checking, k -induction, PDR, Impact, and interpolation-based model checking. This tutorial presents basic use cases for CPAchecker in formal software verification focusing on its main verification techniques with their strengths and weaknesses. The appendix also shows further use-cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to posses a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 2.3.1.