EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)

Abstract

Abstract Thetais 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 toThetabeing unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to createEmergenTheta, a sandbox for the new approaches we wantThetato 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 toEmergenTheta, and its first debut on SV-COMP’24 in the ReachSafety category.