ABSTRACT. Modern stream-based monitors collect detailed statistics of the runtime behavior of the system under observation. If the systems runs in a privacy-sensitive context, this poses the risk of disclosing sensitive information. Differential privacy is the state-of-the-art approach for protecting sensitive information, however, integrating it into runtime monitoring is challenging: temporal operators can cause individual input values to influence multiple outputs over time, leading to repeated disclosure of private information. We propose an approach that automatically enforces differential privacy in stream-based monitoring specifications by analyzing temporal dependencies and injecting carefully calibrated noise into the specification. To preserve the utility of the outputs, we identify strategically chosen positions in the specification for noise injection and leverage tree-based mechanisms to mitigate the accuracy loss caused by noise injected into aggregation operators. We demonstrate the practicality and effectiveness of our approach in a case study on monitoring public transportation usage.

ABSTRACT. This paper presents the first symbolic bounded model checking technique capable of verifying ∀+∃+-liveness hyperproperties (expressed in HyperLTL) over arbitrary (non-terminating) reactive systems. Previous bounded procedures for HyperLTL handled only safety hyperproperties or arbitrary properties over terminating systems. We implement our technique as HyperLasso, and our evaluation results show that it consistently outperforms the explicit-state complete model checker AutoHyper (the only existing tool capable of automatically verifying this class of problems) at several complex bug-finding and synthesis problems.

ABSTRACT. We show how to use passive automata learning to infer models of attacker-defender interactions in cybersecurity. By treating system event logs as words in a formal language, we can apply the RPNI algorithm to infer minimal deterministic finite automata from observed traces. We evaluate this approach through a case study on the Cyber Operations Research Gymnasium (CybORG), a widely-used simulation framework for training defensive agents using machine learning. We analyze the structural properties of the inferred automata and assess their empirical fidelity with respect to the semantics of CybORG. Our results show that accurate formal models can be learned from a relatively small number of traces, suggesting a promising path toward more automated and data-driven approaches to cybersecurity.

ABSTRACT. We introduce the tool HyperQB2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

ABSTRACT. Satisfiability Modulo Theories (SMT) solvers are widely used in formal verification.In program analysis, users often encounter queries that differ only by simple syntactic mutations and are logically equivalent. These mutations typically include assertion reordering, symbol renaming, antisymmetric relation inversion, and commutative operand reordering. However, such minor changes can cause runtimes to vary by orders of magnitude. This variability reduces the predictability required for industrial-scale verification and remains a critical challenge. This paper presents SMTStabilizer, a tool that improves the stability of SMT solvers via context-driven normalization. Since complete input normalization has been shown to be as hard as the graph isomorphism problem, SMTStabilizer adopts an approximate normalization strategy to avoid the high cost of exact normalization. The framework converts formulas into a structured representation and propagates structural information across nodes, so that each node becomes aware of its surrounding context. Using these context information, SMTStabilizer derives a consistent ordering over subformulas. This process yields a nearly canonical form that remains consistent across isomorphic inputs. SMTStabilizer also leverages pruning techniques utilizing the syntactic structure of SMT to reduce the normalization time. An evaluation with Z3 and cvc5 on millions of queries shows that SMTStabilizer improves the solvers' stability to over \(98\%\) under 10 random mutations.

ABSTRACT. Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfiability Modulo Theories (SMT) theory of extensional arrays provides array read and write operators and allows extensionality over arrays. This is sufficient to express many aspects of computer aided verification, but lacks succinctness to efficiently deal with arrays that are initialized with a default value. Existing procedures for extending the SMT-LIB theory of arrays with support for constant arrays are limited to arrays with infinite index domains, and existing implementations in SMT solvers only support a fragment of the theory for finite index domains. In this paper, we present a novel decision procedure for the theory of arrays with constant arrays that supports arbitrary index domains and is not limited to the infinite case. We present our procedure as an abstract calculus and show its refutational and satisfiability soundness. We implement a decision procedure based on our calculus in the state-of-the-art SMT solver Bitwuzla and evaluate its performance on a diverse collection of benchmarks and use cases.

ABSTRACT. We generalize an efficient automata-based approach to string constraint solving–the stabilization-based method behind the solver Z3-Noodler–to support relational constraints represented by finite-state transducers (useful, for example, for modelling replaceAll constraints). We focus on an efficient treatment of length constraints by reducing the need for expensive concatenation elimination, which is a major bottleneck in automata-based string solving. We also propose powerful heuristics that significantly improve performance in practice. Implemented on top of Z3-Noodler, our method vastly outperforms existing solvers on benchmarks with relational constraints–it solves more instances and runs orders of magnitude faster.

ABSTRACT. Lagrangian-based duality, traditionally applied in optimization, has recently been generalized to serve as the basis for a unifying framework for primal-dual search algorithms in the context of program verification and automated reasoning. In this paper, we analyze Quantified Satisfiability Modulo Theories (QSMT) algorithms using this framework. Interestingly, our Lagrangian-based analysis reveals that three recently proposed algorithms for quantified linear real arithmetic (LRA) share a common structure, and that their main differences lie in the approach to a certain problem, namely model-based projection for \(\exists\forall\)-formulas. Moreover, in the course of this Lagrangian-based analysis, we identify an issue with the progress property of one of the algorithms, propose a way to fix the issue, and experimentally demonstrate that the proposed fix improves performance.

ABSTRACT. This tool paper presents the latest (2026) version of Mallob – a distributed platform for automated reasoning on demand. Mallob features a world-leading distributed SAT solving engine, which is the first of its kind that supports proof checking, incremental SAT queries, and flexible (re-)scheduling of computational resources. Exploiting this technology, Mallob features further engines relevant for verification, such as MaxSAT and SMT solving. We present these use cases, discuss a wide range of experimental results, and reflect on the system’s impact.

ABSTRACT. In imperative and object-oriented languages, programmers often define relations such as equality or orderings between instances of structs or classes. These object relations must satisfy well-known algebraic properties, such as reflexivity, transitivity, etc. Violations may cause standard library components, such as collections, to behave incorrectly. Crucially, these properties must hold across types, for instance, when comparing instances of different classes. However, studies show that they are commonly violated, and existing techniques for verifying them are non-modular; they give no guarantees if any types are present at runtime that were not known at verification time. Our key idea is to express algebraic properties in a novel, expressive normal form that allows us to statically identify, for each type $T$ and relation $R$, a set of other types that are relevant for the correctness of $R$ in $T$. We prove the intended algebraic properties of $R$ between $T$ and each type in this set. This approach is generic: it applies to different relations (such as equality and orderings), to various imperative and object-oriented languages, and to multiple program logics. We show how it can be used in standard deductive verification tools by encoding the relevant proof obligations using a simple source-to-source rewriting. We implement our technique for the equality relation in the Python verifier Nagini and evaluate it on challenging benchmarks using both Nagini and Dafny, demonstrating its practical applicability and effectiveness.

ABSTRACT. We present ZipLex, a verified framework for invertible linear-time lexical analysis following the longest match semantics. Unlike past verified lexers that focus only on satisfying the semantics of regular expressions and the longest match property, ZipLex also guarantees that lexing and printing are mutual inverses. Thanks to verified memoization, it also ensures that the lexical analysis of a string is linear in the size of the string. Our design and implementation rely on two sets of ideas: (1) a new abstraction of token sequences that captures the separability of tokens in a sequence while supporting their efficient manipulation, and (2) a combination of verified data structures and optimizations, including Huet’s zippers and memoization with a verified imperative hash table. We implemented and verified ZipLex using the Stainless deductive ver- ifier for Scala. Our evaluation demonstrates that ZipLex supports real- istic applications such as JSON processing and lexers of programming languages, and behaves linearly even in cases that make flex-style ap- proaches quadratic. ZipLex is two orders of magnitude faster than Ver- batim++, showing that verified invertibility and linear-time algorithms can be developed without prohibitive cost. Compared to Coqlex, ZipLex also offers linear (instead of quadratic) time lexing, and is the first lexer that to come with invertibility proofs for printing token sequences.

ABSTRACT. Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of verifying operations proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.

ABSTRACT. We present the Cooperating Proof Calculus (CPC), an evolving set of proof rules encompassing all inferences used in the mainstream features of the SMT solver cvc5. CPC consists of 585 proof rules, which weformalized in roughly 6400 lines of definitions in the logical framework Eunoia. Eunoia proofs are independently checkable by the proof checker Ethos. This paper gives a detailed summary of CPC, surveying its proof rules over its major components. Having instrumented cvc5 to generate CPC proofs in Eunoia, we show that the solver is capable of generating fine-grained CPC proofs, with no proof holes, for all benchmarks in the SMT library except those in logics with floating points, which are currently not supported. This results in roughly 913 million proof steps using 427 unique proof rules. We also discuss ongoing work in the proof assistants Lean and Isabelle to verify the correctness of CPC.

ABSTRACT. Burrow is a proof framework for weak memory mapping proofs. Those mappings appear as optimizations and translations between languages inside compilers and binary translators. However, their mechanized proofs, when defined over formal axiomatic weak memory semantics, are often large and complex. In this paper, we discuss the proof primitives provided by Burrow which simplify mechanizing those mapping proofs and help to prove many lemmas generally. To demonstrate the benefits of these primitives, we use Burrow to prove a conjectured mapping from x86 to Arm correct.

ABSTRACT. We present Velvet—a Dafny-style verifier for imperative programs embedded in the Lean proof assistant. Like Dafny, Velvet supports reasoning about effectful programs featuring mutable state, loops, and non-determinism. Unlike Dafny, Velvet seamlessly combines automated SMT-based proofs with the interactive proof mode of the Lean proof assistant, in which it is embedded, thus enabling multi-modal proofs. Implemented as a Lean library, Velvet enjoys interaction with the rest of the Lean ecosystem, and in particular, with its automation tactics and rich library of mathematical theories. In this paper, we give a tour of Velvet’s features, outline the techniques underlying its implementation, and evaluate its performance and expressivity in comparison with Dafny.

ABSTRACT. Separation logic proofs of heap-manipulating programs require careful accounting of objects and pointers in memory. On paper, these proofs are often accompanied by heap memory diagrams that help authors and readers visualize and track the evolution of the program's abstract state. However, users of interactive theorem provers must instead work with plain-text notations that obscure object relationships. This paper presents the first automatic visualization and animation library for separation logic heap predicates. Four key features make the library practical. First, it supports animating across proof steps. Second, it offers a DSL to specify how custom user-specified predicates should be visualized. Third, it is straightforward to port to new separation logic frameworks. And fourth, it can be used in browsers and IDEs, during and after proof development. We demonstrate these features by implementing frontends for CFML and Iris, integrating with Alectryon and VsRocq, and reproducing hand-drawn diagrams found in published materials.

ABSTRACT. A DFA separates two disjoint languages $L_1$ and $L_2$ if it accepts every word in $L_1$ and rejects every word in $L_2$. Algorithms for active learning of small separating DFAs have many applications, e.g.\ for learning network invariants, learning contextual assumptions in compositional verification, learning state machines from large amounts of log data, and learning bug pattern descriptions. In this paper, we propose a new learning algorithm, inspired by $L^{\#}$, that learns a minimal separating DFA for disjoint languages $L_1$ and $L_2$ if one exists. Experimental results show that our algorithm significantly outperforms existing active learning algorithms on both randomly generated and industrial benchmarks.

ABSTRACT. Emerson-Lei automata, which allow arbitrary Boolean combinations of $\mathtt{Fin}$ and $\mathtt{Inf}$ acceptance conditions, provide a unifying framework for $\omega$-automata but pose significant challenges for determinization. The previous best algorithm relies on a \texttt{removeFin} transformation that introduces an exponential blow-up in the state space before determinization even begins. We present a new determinization algorithm that completely bypasses this bottleneck. Our key insight is that each disjunct of an Emerson-Lei condition in DNF corresponds directly to a \emph{one-Fin automaton}---a restricted form of Streett automaton whose structure enables more efficient determinization via H-Safra trees. By exploiting this connection, we establish an upper bound of \[ 2^{O\!\big(3^{|\alpha|/3} \cdot (n \log n + n|\alpha| \log |\alpha|)\big)} \] where $n$ is the number of states and $|\alpha|$ is the acceptance condition size. This improves the exponent over the previous best bound by a factor of $2^{2|\alpha|}/3^{|\alpha|/3}$, an exponential improvement in the acceptance condition complexity.

ABSTRACT. We present an SMT-based active learning algorithm for non-deterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/L*-style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to produce minimal WFAs. We prove partial correctness and provide a sufficient termination condition, which in particular implies termination for all finite semirings. Our extensive experimental evaluation shows that our algorithm is capable of learning numerous minimal WFAs over both finite and infinite semirings, vastly outperforms a naive baseline, and is competitive with a state-of-the-art algorithm while producing significantly smaller automata and requiring less interaction with the teacher.

ABSTRACT. In many verification tasks, system models do not correspond to the focused and idealized models that appear in research literature. In practice, models usually contain components and execution paths that are irrelevant to the property being verified or have only a minor effect on it. Compositional verification presents a practical method for coping with the larger and less targeted models found in such settings. In this paper, we present an automated compositional framework for verifying timed safety properties in networks of timed automata. We show as a main result that the weakest environment assumption, commonly used in compositional reasoning, may in general fail to be recognizable within the timed automata formalism. This negative result motivates shifting the focus to the complement language of violation-inducing timed words, for which we establish recognizability using timed automata with silent transitions. We provide an algorithm for its construction and reduce its size by retaining only the parts directly relevant to the property. The synthesized assumption is later applied to verify the original system. This provides a sound and complete basis for compositional verification of timed automata, including the novel ability to handle automata with multiple clocks and non-deterministic behavior. Our results broaden the applicability of assume–guarantee verification techniques in timed automata and show substantial reductions in the size of the state-space, outperforming monolithic methods on a range of case studies.

ABSTRACT. Workflow nets are a variant of Petri nets used for modelling business processes. Central decision problems are soundness problems; one popular variant is called generalised soundness. These problems intuitively ask whether initiated processes can be finalised. We introduce weighted soundness, which strengthens the classical concepts of soundness. In weighted soundness, we bound the weight (typically length) of runs to finalise processes. This allows one to require processes to be finalised within a restricted budget. We provide multiple reasons supporting the relevance of weighted soundness. Our theoretical analysis shows that weighted soundness is provably simpler than classical soundness. Our main result is that weighted generalised soundness is co-NP^NP-complete, while (unweighted) generalised soundness is known to be PSPACE-complete. Our practical analysis shows that on standard benchmarks classical soundness coincides with weighted soundness, if the weight is set to the number of transitions in the workflow net. Furthermore we analyse the Inductive Miner algorithm, one of the most popular algorithms generating workflow nets from event logs. Inductive Miner is known to guarantee the output workflow nets to be generalised sound. We show that it outputs workflow nets that are weighted generalised sound with a weight linear in the size of the event alphabet. Finally, we generalise reduction techniques from soundness to weighted soundness. Such reductions are crucial in implementations of soundness algorithms.

ABSTRACT. Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin’s L* algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems.

ABSTRACT. We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.

ABSTRACT. Quantitative automata (QAs) extend finite-state $\omega$-automata with weighted transitions to specify quantitative system properties. However, their finite weight sets rule out properties like average response time, where response times can be arbitrarily large. Nested quantitative automata (NQAs) overcome this limitation: a parent automaton spawns child automata to compute unbounded values over finite subwords and aggregates them into a final result. Despite this expressiveness, NQAs have lacked practical tool support to date. We address this gap by extending the Quantitative Automata Kit (QuAK), a software tool for QA analysis, to support NQAs. Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging QuAK's existing decision procedures. The tool handles all decidable combinations of parent aggregators (including limits and averages) and child functions (extrema and monotonic or bounded summations). Experiments on response-time and resource-consumption benchmarks demonstrate QuAK's effectiveness.