Theta

About

Theta is a generic, modular and configurable model checking framework developed at the Critical 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. Theta can both serve as a model checking backend, and also includes ready-to-use, stand-alone tools.

Use Theta

Tools are concrete instantiations of the framework to solve a certain problem using the built-in algorithms. Currently, the following tools are available (follow the links for more information).

• theta-cfa-cli: Reachability checking of error locations in Control Flow Automata (CFA) using CEGAR-based algorithms.
  • Gazer is an LLVM-based frontend to verify C programs using theta-cfa-cli, also giving support towards SV-COMP. See our tool paper at TACAS for more information.
  • PLCverif is a tool developed at CERN for the formal specification and verification of PLC (Programmable Logic Controller) programs, supporting theta-cfa-cli as one of its verification backends.
• theta-sts-cli: Verification of safety properties in Symbolic Transition Systems (STS) using CEGAR-based algorithms.
  • theta-sts-cli natively supports the AIGER format of the Hardware Model Checking Competition (HWMCC).
• theta-xta-cli: Verification of Uppaal timed automata (XTA).
• theta-xsts-cli: Verification of safety properties in eXtended Symbolic Transition Systems (XSTS) using CEGAR-based algorithms.
  • Gamma is a statechart composition framework, that supports theta-xsts-cli as a backend to verify collaborating state machines.
  • theta-xsts-cli natively supports Petri net models in the PNML format (experimental).
• theta-xcfa-cli: Reachability checking of error locations in eXtended Control Flow Automata (XCFA) using CEGAR-based algorithms. The CFA formalism is extended with procedures and processes, able to support multithreaded analysis and also several optimization passes. Right now it is mainly used to check both single and multithreaded C programs.
  • the c-frontend module of Theta is capable of parsing C programs and transforming them into a formalism independent, in-memory representation. The xcfa-cli is able to convert this representation into an XCFA.

Overview of the architecture

Theta can be divided into the following four layers.

• Formalisms: The core elements of Theta are the formalisms, which represent models of real life systems (e.g., software, hardware, protocols). Formalisms are usually low level, mathematical representations based on first order logic expressions and graph like structures. Formalisms can also support higher level languages that can be mapped to that particular formalism by a language front-end (consisting of a specific parser and possibly reductions for simplification of the model). The common features of the different formalisms reside in the core project (e.g., expressions and statements) and each formalism has its own project. Currently, the following formalisms are supported: (extended) symbolic transition systems (sts / xsts), control-flow automata (cfa) and timed automata (xta).
• Analysis back-end: The analysis back-end provides the verification algorithms that can formally prove whether a model meets certain requirements. There is an interpreter for each formalism, providing a common interface towards the algorithms (e.g., calculating initial states and successors). This ensures that most components of the algorithms work for all formalisms (as long as they provide the interpreter). The verification algorithms are mostly based on abstraction. The analysis back-end defines various abstract domains (e.g., predicates, explicit values, zones), strategies for performing abstraction and refinement (e.g., interpolation), and algorithms built from these components. The common components reside in the analysis project (e.g., CEGAR loop) and the formalism-specific modules (e.g., the interpreters) are implemented in separate analysis projects (with suffix -analysis) for each formalism.
• SMT solver interface and SMT solvers: Many components of the algorithms rely on satisfiability modulo theories (SMT) solvers. The framework provides a general SMT solver interface in the project solver that supports incremental solving, unsat cores, and the generation of binary and sequence interpolants. Currently, the interface is implemented by the Z3 SMT solver in the project solver-z3, but it can easily be extended with new solvers.
• Tools: Tools are command line applications that can be compiled into a runnable jar file. Tools usually read some input and then instantiate and run the algorithms. Tools are implemented in separate projects, currently with the -cli suffix.

The table below shows the architecture and the projects. Each project contains a README.md in its root directory describing its purpose in more detail.

	Common	CFA	STS	XTA	XSTS	XCFA
Tools	solver-smtlib-cli	cfa-cli	sts-cli	xta-cli	xsts-cli	xcfa-cli
Analyses	analysis	cfa-analysis	sts-analysis	xta-analysis	xsts-analysis	xcfa-analysis
Formalisms	core, common	cfa	sts	xta	xsts	xcfa
SMT solvers	solver, solver-z3, solver-smtlib

Extend Theta

If you want to extend Theta and build your own algorithms and tools, then take look at doc/Development.md.

Read more

If you want to read more, take a look at our list of publications. A good starting point is our tool paper and slides/talk presented at FMCAD 2017. Furthermore, our paper in the Journal of Automated Reasoning is a good overview of the algorithms in Theta.

To cite Theta as a tool, please use the following paper.

@inproceedings{theta-fmcad2017,
    author     = {T\'oth, Tam\'as and Hajdu, \'{A}kos and V\"or\"os, Andr\'as and Micskei, Zolt\'an and Majzik, Istv\'an},
    year       = {2017},
    title      = {Theta: a Framework for Abstraction Refinement-Based Model Checking},
    booktitle  = {Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design},
    isbn       = {978-0-9835678-7-5},
    editor     = {Stewart, Daryl and Weissenbacher, Georg},
    pages      = {176--179},
    doi        = {10.23919/FMCAD.2017.8102257},
}

Acknowledgements

Supporters of the Theta project are listed below.

• MTA-BME Lendület Cyber-Physical Systems Research Group
• Fault Tolerant Systems Research Group, Department of Measurement and Information Systems, Budapest University of Technology and Economics
• Gedeon Richter’s Talentum Foundation
• Nemzeti Tehetség Program, Nemzet Fiatal Tehetségeiért Ösztöndíj 2016 (NTP-NFTÖ-16)
• Nemzeti Tehetség Program, Nemzet Fiatal Tehetségeiért Ösztöndíj 2018 (NTP-NFTÖ-18)
• CECRIS project (EU FP7 324334)
• R5-COP project (EU FP7 ARTEMIS 621447 and NRDI Fund NEMZ_12-1-2014-0003)
• Arrowhead Tools project (EU ECSEL 826452 and NRDI Fund 2019-2.1.3-NEMZ_ECSEL-2019-00003)