Changes from CPAchecker 1.9.1 to CPAchecker 2.0 Better support for Windows We now bundle binaries of SMT solvers like MathSAT and Z3 for Windows, such that most configurations of CPAchecker work on Windows out of the box. REUSE compliance CPAchecker now follows the licensing best practices of the FSFE and is REUSE compliant, i.e., everything in the repository is labeled with machine-readable headers that include copyright and license information. This makes it easy to check the licenses of all CPAchecker-internal and third-party components and ensure that all requirements such as bundling license texts and copyright notices are fulfilled when redistributing CPAchecker. More information about the license status can be found in README.md. Interpolation-based Model Checking (IMC) A new reachability-safety analysis (config -bmc-interpolation), which adopts a state-of-the-art verification algorithm for hardware proposed by McMillan (cf. "Interpolation and SAT-Based Model Checking". K. L. McMillan. In Proc. CAV, Springer, 2003) to software, has been added to CPAchecker. Automated Fault Localization CPAchecker now supports multiple techniques for automatic fault-localization. If fault localization is enabled and CPAchecker finds a counterexample during analysis, CPAchecker will mark likely faults in the program that lead to that counterexample. Fault-localization results are presented in the produced HTML reports (Counterexample.*.html). The following fault-localization configurations exist: Coverage-based fault localization: -setprop analysis.algorithm.faultlocalization.by_coverage=true Interpolation-based fault localization: -setprop analysis.algorithm.faultlocalization.by_traceformula=true Distance metrics: -setprop analysis.algorithm.faultlocalization.by_distance=true