Dieses Kapitel untersucht den Verifikationsansatz von EmergenTheta, einem Werkzeug, das C-Programme in erweiterte Kontrollflussautomaten und symbolische Übergangssysteme zur Analyse verwandelt. Es setzt eine Reihe von Algorithmen ein, darunter die Überprüfung begrenzter Modelle, K-Induktion und interpolationsbasierte Modellüberprüfung, wobei eine neuartige Ergänzung entscheidungsdiagrammbasierter Algorithmen wie Substitutionsdiagramme und Sättigungstechniken hinzukommt. Die in Kotlin und Java geschriebene Architektur des Tools integriert sich in das Theta-Framework und unterstützt mehrere SMT-Solver. EmergenTheta nahm an SV-COMP '25 teil und demonstrierte seine Fähigkeit, verschiedene Eigenschaften wie unerreichbare Anrufe, Terminierung und kein Überlaufen zu handhaben. In diesem Kapitel werden die Stärken des Tools diskutiert, einschließlich seiner breiten Verifikationsreichweite und der vielversprechenden Ergebnisse des neuen GSAT-Algorithmus. Allerdings räumt sie auch Schwächen ein, wie den falschen Umgang mit Fließkomma-NaN-Werten und die Aufsicht bei der Umsetzung des Portfolios. Das Kapitel schließt mit Empfehlungen zur Einrichtung und Konfiguration von Werkzeugen, die einen umfassenden Überblick über die Fähigkeiten und Bereiche von EmergenTheta für zukünftige Verbesserungen bieten.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
EmergenTheta is our sandbox for experimental analyses. After its successful debut in SV-COMP’24, we kept some well-performing but still under-tested configurations, and complemented them with a new saturation algorithm over decision diagrams, and two ways of extending their verification power: wrapping them in a lightweight, counterexample-guided abstraction refinement (CEGAR) loop based on implicit predicate abstraction; and backwards traversal of the state space. All such analyses now rely on a common interface to the underlying symbolic transition system, integrating seamlessly into the existing Theta framework. Using this combination of proven analyses and novel extensions, EmergenTheta outperformed our expectations in SV-COMP’25.
Hinweise
Levente Bajczi: Jury member representing EmergenTheta at SV-COMP 2025.
Fig. 1.
Overview of the verification approach of EmergenTheta. 2025 additions are denoted with the \(\bigstar \) symbol. Parts irrelevant to SV-COMP are grayed out.
1 Verification Approach
EmergenTheta parses the C programs and transforms them into the extended control flow automaton (XCFA) formalism through a series of preprocessing steps. XCFA are then transformed into the low-level symbolic transition system (STS) formalism, which captures the model behavior using two SMT formulas, one characterizing the initial states and the other characterizing the transition relation.
Anzeige
Bounded model checking (BMC) [8] can prove the faultiness of a model by constructing path constraints that characterize all possible counterexamples of a given length k and checking the satisfiability of such constraints using an SMT solver. The bound k is incremented until either the model is proven unsafe, or until the available resources allow. K-induction (K-IND) [17] and interpolation-based model checking (IMC) [13] extend BMC with additional checks in an attempt to prove that the model is safe. K-induction does so by trying to prove the k-inductivity of the property with k being the current BMC length, while IMC derives Craig interpolants to compute an overapproximation of the set of reachable states.
Decision-diagram-based algorithms are a novel addition to the set of available algorithms this year. Substitution diagrams [15] allow us to handle SMT formulas as multi-valued decision diagrams (MDDs) in a top-down approach supported by efficient caching and lazy evaluation for the presence of edges. Using substitution diagrams, we can represent the states and transitions of the system with MDDs constructed from the SMT formulas of the STS representation. The saturation algorithm [9] can compute the set of reachable states on decision diagrams in a bottom-up manner. It decomposes the exploration into smaller explorations on submodels exploiting the locality of the system’s events. The generalized saturation (GSAT) [14] algorithm employs a weaker notion of locality to further enhance the saturation effect.
The modular architecture of EmergenTheta also allows us to wrap the aforementioned analyses into a CEGAR loop based on implicit predicate abstraction [18] and to traverse the state space in a reversed manner.
We run the aforementioned analyses in a sequential portfolio. We start with the GSAT algorithm (because it can find a safety proof fairly quickly, or report the task not solvable with the configuration), then move on to BMC and K-Induction. Afterwards, we intended to start the abstracted and reversed IMC, but ended up using K-Induction due to a bug (see Sect. 3).
Anzeige
2 Software Architecture
EmergenTheta is a JVM-based tool, written primarily in Kotlin (and legacy parts of the code are written in Java).
EmergenTheta is part of the Theta framework [12], and can therefore use its integrated frontend- and solver-infrastructure. Parsing C files is done using a custom ANTLR grammar [2]. Satisfiability Modulo Theories (SMT) solvers can be invoked three different ways:
Z3 [16] is natively integrated, its Java API is a dependency of Theta
Other solvers are integrated via SMT-LIBv2 [11], such as MathSAT5 [10] or CVC5 [5]
JavaSMT [1] has been integrated since last year’s SV-COMP
In SV-COMP’25, we use Z3, MathSAT5, and CVC5.
Fig. 2.
Successful verification results per configuration
3 Discussion of Strengths and Weaknesses of the Approach
EmergenTheta took part in SV-COMP’25 with 3 checkable properties: the conventional unreach-call (as previously [3]); and we debuted with termination and no-overlow this year using a pre-processing step using TransVer [7]. This broadened verification reach is a definitive strength of our tool, but cannot be attributed to its architecture, as the pre-processing step is transparent to EmergenTheta. In the future we plan to integrate it into our portfolio more, as experiences with reachability need not translate to other properties when it comes to verification efficacy (based on results in Figure 2 [6]).
It is also worth mentioning that a large number of tasks (232 for no-overflow, 51 for termination, but only 1 for unreach-call) were solved by sanity checks before a verifier algorithm was started. In these instances safety was evident, as in the control flow graph, we do not have any paths from the initial location to the error locations.
Unfortunately, the portfolio implementation contained an oversight, making IMC-based analyses become K-Induction-based analyses by mistake. This is reflected in our results: we wanted to run IMC with abstraction and with reversal, but ended up running K-Induction in these instances, and these represent our least efficient configurations (see Figure 2). We will move to a more robust portfolio-engine in the future so that oversights like this can be more easily avoided. However, both abstraction and reversal solved tasks that the non-reversed and not-abstracted configurations did not, therefore, we are confident in their advantages overall.
The new algorithm, GSAT, produced really promising results this year. It proved safety in 152 tasks, and found a bug in 33 instances. However, it could only output correctness witnesses this year, and no violation witnesses, so the 33 successful verification tasks are correct, but unconfirmable.
EmergenTheta produced a few wrong results. In the unreach-call category it produced 2, in termination 20, and in no-overflow 15 false positive results. It produced no false negative (false safe) results. The cause of the wrong results are partly due to a mishandling of floating point NaN values, and due to the preprocessing step mapping the new properties to reachability.
4 Tool Setup and Configuration
EmergenTheta is widely configurable, and choosing a successful configuration for a verification task at hand can be complicated. If using the competition archive [4] for software verification, we recommend using the following input options, starting our EMERGENT portfolio:
To minimize the output verbosity, the option –loglevel RESULT can be added to the arguments. We also used these options at SV-COMP 2025.
5 Software Project and Data-Availability Statement
EmergenTheta is integrated into the Theta verification framework maintained by the Critical Systems Research Group1 of the Budapest University of Technology and Economics. The project is available open-source on GitHub under an Apache 2.0 license2, and the binary release of the competition version (6.8.6) is published on Zenodo [4].
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
