Theta is a general, modular and configurable model checking framework developed at the Critical Systems Research Group (BME, ftsrg) of the Budapest University of Technology and Economics, with the aim of supporting the design and understanding of algorithms based on abstraction refinement for the accessibility analysis of different formalisms. The main distinguishing feature of Theta is its architecture, which allows the definition of input formalisms with a higher-level language front-end, as well as the combination of different abstract domains, interpreters, and abstraction-refinement strategies. Theta can simultaneously serve as a model-checking backend, and includes ready-made, independent tools.

The topic includes theoretical and practical developments, algorithm development, implementation and proof related to the Theta framework. Optimization of existing implementations, exploration of new directions, and algorithm implementation based on recent scientific results can be carried out within the framework of this topic.