Theta is a model checking framework, with a strong emphasis on effectively handling
concurrency in software using abstraction refinement algorithms. In SV-COMP 2024,
we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction
technique; and 3) enhanced support for call stacks to handle recursive programs. We
integrate these techniques in an improved architecture with inherent support for portfolio-based
verification using dynamic algorithm selection, with a diverse selection of supported
SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent
and recursive software support.
