analysis

README.md — what this module is

Mirrored from subprojects/common/analysis/README.md — edit it there, not here.

This project contains the analysis algorithms and their components, e.g., abstract domains, abstract reachability graphs, refinement strategies, precisions, etc. The formalism specific components ( e.g., the interpreter) are implemented in separate projects for the given formalism.

Further reading

The full publication list is at theta.mit.bme.hu/publications.

CEGAR

• A Configurable CEGAR Framework with Interpolation-based Refinements (FORTE 2016) — the configurable CEGAR framework this project implements.
• Efficient Strategies for CEGAR-based Model Checking (JAR 2020) — the reference paper for the configuration options; see also CEGAR-algorithms.md.
• A Survey on CEGAR-based Model Checking (MSc, 2015).
• Exploratory Analysis of the Performance of a Configurable CEGAR Framework (Minisy 2017) and A Preliminary Analysis on the Effect of Randomness in a CEGAR Framework (Minisy 2018) — how configuration and randomness affect performance.

Abstract domains (expl/, pred/, prod2/)

• Software Model Checking with a Combination of Explicit Values and Predicates (Minisy 2019).
• Combining Abstract Domains for Software Model Checking (BSc, 2018) and Efficient combinations of predicate abstraction and explicit-value analysis (MSc, 2020).

Beyond CEGAR (algorithm/ic3, algorithm/mdd, algorithm/bounded)

• Applying Incremental, Inductive Model Checking to Software (BSc, 2018) — IC3 on software, via a transformation to a symbolic transition system.
• EmergenTheta: Variations on Symbolic Transition Systems (SV-COMP 2025) — the monolithic-expression encodings shared by BMC/k-induction/IMC, IC3 and MDD.
• EmergenTheta: Experimental Analyses within the Theta Framework (SV-COMP 2026) — combined predicate-explicit domain, on-the-fly reachability and counterexample generation for generalized saturation, and an IC3 backend.
• Saturation Enhanced with Conditional Locality: Application to Petri Nets (PETRI NETS 2019) — explains saturation, which has been generalized from just Petri nets in Theta.

Liveness / LTL (algorithm/loopchecker, multi/)

• Abstraction-Based Model Checking of Linear Temporal Properties (Minisy 2020) — CEGAR combined with automata-theoretic LTL checking, and the interpolation-based refinement of lasso-shaped counterexamples.

Runtime monitoring (runtimemonitor/)

• Extending the Capabilities of the CEGAR Model Checking Algorithm (MSc, 2023) — detecting and mitigating non-progressing refinement loops.

Pointers (ptr/)

• Giving Some Pointers for Abstraction-Based Model Checking (Minisy 2025) — tracking predicates over abstract memory locations.