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

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. © The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.