Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)

International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)


Theta is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.

Latest Publications