v4.2.3

Auto-generated release

SVCOMP23 release

SV-COMP 2023 submission

This release contains binaries for the 2023 SV-COMP competition.

Minimal necessary packages for Ubuntu 22.04 LTS:

• openjdk-17-jre-headless
• libgomp1
• libmpfr-dev

Contents of the Submission

.
├── CONTRIBUTORS.md - contains information on the main contributors to Theta
├── LIB_LICENSES.md - contains the licensing information for packaged dependencies
├── LICENSE - contains the license for Theta
├── README.md - this file
├── complex.kts - the portfolio script used this year
├── lib - contains the library dependencies
│   ├── libmpfr_java-1.0.so
│   ├── libz3.so
│   └── libz3java.so
├── solvers - contains further dependencies (SMT-solvers), each having their respective licenses attached
│   ├── bitwuzla
│   │   └── 3ea759df11285e722b565c0b5c132dc0bb77066f
│   ├── cvc5
│   │   └── 1.0.2
│   ├── mathsat
│   │   ├── 5.6.8
│   │   └── fp
│   ├── princess
│   │   └── 2022-07-01
│   ├── smtinterpol
│   │   └── 2.5-1230
│   └── z3
│       ├── 4.10.1
│       └── 4.11.2
├── theta-smtlib.jar - the jarfile for installing and managing smt solvers (not necessary unless different solver versions are required)
├── theta-start.sh - the starting script of Theta
└── theta.jar - the main jarfile of Theta

Usage

This packaged version of Theta is equipped with the necessary SMT solvers, libraries and binary version of Theta. To use it, one has to simply execute theta-start.sh with the desired parameters. The first parameter must be the name of the input task (except when using --version). The script provides the --smt-home directory to Theta.
The tool is used with the following parameters on SV-Comp 2023:

--witness-only \
--portfolio COMPLEX \
--loglevel RESULT

For a more verbose output, change --witness-only to --output-results and --loglevel to MAINSTEP, SUBSTEP, INFO or DETAIL.
For more parameters, check out the documentation on CEGAR (might not be up to date on every parameter, but gives a detailed explanation on them) and the main class of the XCFA frontend.

v4.2.2

This release adds "no refinement progress detection" to the XSTS cli.
(Turning it off is possible with the --no-stuck-check flag)

v4.2.1

This release fixes a bug related to local variables in the XSTS formalism.

v4.2.0

This release adds basic function support to Theta, meaning it can now verify recursive programs. The previously used function inlining can be turned back on with the --inline ON flag.

v4.1.0

The new release contains a partial order reduction algorithm for multi-threaded programs. The algorithm has a formalism-independent core (PorLts), and an implementation for the XCFA interleavings algorithm (XcfaPorLts). POR can be enabled with the --algorithm INTERLEAVINGS_POR flag.

v4.0.0

This release adds many important changes to Theta. The most important ones:

1. frontends subproject-family adds a place for non-dsl parsers for the formalisms in Theta
2. c-frontend subproject adds support for C programs
3. xcfa subproject-family adds a new formalism, the eXtended Control Flow Automaton to Theta
4. An experimental portfolio and algorithm selection engine for the XCFA formalism
5. An experimental BMC implementation

v3.0.2

This release fixes a bug of ArrayInit expressions.

v3.0.1

This fixes a problem with parsing bitvector extract expressions due to FpType declaration syntax (See issue #148)

SV-COMP'22 v1

This release contains the binaries and the source tree of the version which is submitted to the qualification run of the SV-COMP 2022 competition.

Minimal necessary packages for Ubuntu 20.04 LTS:

• openjdk-11-jre-headless
• libgomp1
• libmpfr-dev

Note: this release might contain unstable features and is NOT built from master.