Theta: a Framework for Abstraction Refinement-Based Model Checking

Theta is a generic, modular and configurable model checking framework developed at the Fault Tolerant Systems Research Group of Budapest University of Technology and Economics, aiming to support the design and evaluation of abstraction refinement-based algorithms for the reachability analysis of various formalisms. The main distinguishing characteristic of Theta is its architecture that allows the definition of input formalisms with higher level language front-ends, and the combination of various abstract domains, interpreters, and strategies for abstraction and refinement.

Source code

  • The source code of the project is available on GitHub.

Tool downloads

The binaries of Theta prototype tools, along with some input models can be downloaded below.

  • theta-sts - a model checker for symbolic transition systems
  • theta-xta - a model checker for UPPAAL timed automata in .xta format
  • theta-cfa [unstable] - a model checker for simple .C programs


See the list of publications.


Check out our flyer.