New CPAchecker version 4.0

[Philipp Wendler]

Dear CPAchecker users,

we are happy to announce the release of CPAchecker 4.0!

Compared to version 3.0, this release brings one major improvement:

The default configuration of CPAchecker is now more advanced and
effective. For standard reachability properties it now uses strategy
selection on program features such as the whether loops exist to choose
a particular analysis. In most cases, a parallel portfolio of a diverse
range of analyses such as k-induction, IMC, predicate abstraction, and
value analysis is used. Parallel portfolios of different analyses are
also used for verification of memory-safety and termination properties.

The remaining release notes:

* Initial support for handling `atexit`.
* The generated HTML report does no longer contain the witness tab by
default. In some cases, it can take a long time to generated.
Set the option `report.addWitness=true` to re-enable it.

For those of you who used the Subversion repository of CPAchecker,
please note that on 2024-10-18 the CPAchecker repository was migrated to
git and is now hosted at
https://gitlab.com/sosy-lab/software/cpachecker/

We would like to thank the many people that have contributed to the
development of CPAchecker!
Their full list is here: https://cpachecker.sosy-lab.org/acknow.php

The new release is as always available at
https://cpachecker.sosy-lab.org/download.php
and as Debian/Ubuntu package on https://apt.sosy-lab.org/.
Our official Docker image is named "sosylab/cpachecker:4.0"
and there is an artifact on Zenodo:
https://zenodo.org/records/14203369

Kind regards
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181