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.

For more information see the GitHub page.