Changes from CPAchecker 1.8 to CPAchecker 1.9 --------------------------------------------- * CPAchecker 1.9 is the last release that works on Java 8, future versions of CPAchecker will require Java 11 or newer. * CPAchecker can now use the new BDD library ParallelJBDD (https://gitlab.com/sosy-lab/software/paralleljbdd) as replacement for JavaBDD if the option `bdd.package = PJBDD` is used. * Support for Cyclic Analysis Combinations Next to sequential combinations and parallel combinations, CPAchecker now also provides an algorithms for cyclic combinations of analyses that can be e.g. be used to interleave analyses or iteratively execute a sequence. of analyses. Different modes are supported. For example, analyses may resume their previous exploration, start from scratch. * Cooperative Verifier-based Testing (CoVeriTest) CoVeriTest uses a cyclic combination of analyses to generate test cases for standard coverage criteria like statement or branch coverage. Also, the coverage properties of the international competition on software testing (Test-Comp) are supported. The specialty of CoVeriTest is that it cannot only configure the analyses participating in test-generation as well as their individual time limits in each iteration, but also which information are exchanged between different analysis runs. For details, we refer to the main CoVeriTest publication: Beyer, D.; Jakobs, M.-C.: CoVeriTest: Cooperative Verifier-Based Testing. In: Proc. FASE, Springer, 2019. CoVeriTest also participated in Test-Comp'19 and won the 3rd place.