Mirrored page
Mirrored from doc/Tools.md — edit it there, not here.
Tool variants
Theta is submitted to competitions under several tool names. They are packaging variants of
xcfa-cli, differing in the portfolio they run and the solvers they ship (see the variant { … }
blocks in xcfa-cli/build.gradle.kts); the
archived artifacts are linked from the repository README.
| Tool | Variant | Portfolio |
|---|---|---|
| Theta | Theta-svcomp |
the default portfolio of abstraction-refinement analyses |
| EmergenTheta | EmergenTheta-svcomp |
emerging (not yet mature) analyses |
| SymbolicTheta | SymbolicTheta-svcomp |
--portfolio SYMBOLIC: generalized saturation over MDDs, aimed at concurrency |
| Thorn | Thorn-svcomp |
--portfolio HORN: software verification via CHC encoding (Eldarica, Golem, Z3) |
| ThetaCHC | Theta-chccomp |
CHC-COMP entry; see chc-frontend |
Further reading
The full publication list is at theta.mit.bme.hu/publications.
- EmergenTheta: Verification Beyond Abstraction Refinement (SV-COMP 2024) — why EmergenTheta exists: a sandbox separating emerging techniques from the mature ones, so that new approaches can be tried without hurting the reliability of the main tool.
- EmergenTheta: Variations on Symbolic Transition Systems (SV-COMP 2025).
- EmergenTheta: Experimental Analyses within the Theta Framework (SV-COMP 2026) — first submission to all categories.
- Theta: Abstraction Based Techniques for Verifying Concurrency (SV-COMP 2024) and Theta: Various Approaches for Concurrent Program Verification (SV-COMP 2025).
- Theta as a Horn Solver (HCVS 2025) — ThetaCHC in CHC-COMP.