EmergenTheta: Experimental Analyses within the Theta Framework (Competition Contribution)

Abstract EmergenTheta is our sandbox for emerging analyses within the Theta framework. Previously established analyses have been migrated to Theta , and EmergenTheta focuses exclusively on novelties for both counterexample-guided abstraction refinement over control-flow automata and reachability analyses over symbolic transition systems. The 2026 submission presents a combined predicate–explicit abstraction domain, multithreaded symbolic transition system encodings, on-the-fly reachability and counterexample generation for generalized saturation, and an IC3 backend. This is the first year that we were able to submit EmergenTheta to all categories, representing a significant step in the evolution of Theta , and the competition results indicate the practical viability of the new techniques.