Theta is a model checking framework conventionally based on abstraction refinement
techniques. While abstraction is useful for a large number of verification problems,
the over-reliance on the technique led to Theta being unable to meaningfully adapt.
Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta
, a sandbox for the new approaches we want Theta to support. By differentiating between
mature and emerging techniques, we can experiment more freely without hurting the
reliability of the overall framework. In this paper we detail the development route
to EmergenTheta , and its first debut on SV-COMP’24 in the ReachSafety category.