ABSTRACT. Consistency-based diagnosis is a formal approach to software fault localization that explains failing executions by identifying program components whose modification would restore correctness. Tools such as BugAssist and (more recently) CFaults instantiate this idea using logical encodings and bounded model checking. In our first contribution, we improve on this line of work. We present SherLoc, a consistency-based diagnosis engine for ANSI-C programs with multiple failing test cases. SherLoc introduces an explicit repair model that supports pointers and arrays, ensuring that diagnoses correspond only to semantically valid C repairs. In addition, we adapt efficient algorithms from hardware diagnosis, which avoid costly self-composition, and significantly outperform existing tools on standard benchmarks. In our second contribution, we expose fundamental limitations of formal fault localization: program optimizations and transformations can invalidate diagnoses despite semantic equivalence, representing a major hurdle to further scalability improvements; function inlining can break the functional consistency of repairs, yielding diagnoses that cannot be realized at the source level; and bounded encodings inherently miss diagnoses in the presence of loops or unbounded behavior. Our exposition clarifies the gap between the formal ideal of sound and complete diagnosis and what current techniques can realistically guarantee, and thereby helps guide future work toward more robust and principled approaches.

ABSTRACT. We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto industrial C++ codebases where correctness arguments are embedded within implementation artifacts. We focus on a formal analysis of the core SDEX algorithm which implements the Stellar blockchain’s order-book. By combining Large Language Models, the Prototype Verification System (PVS) and Seahorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of interactive theorem proving and model checking provides a path for delivering actionable assurance to legacy, high-value systems.

ABSTRACT. SvLibChecker is a small tool for software model checking. The goal of the tool is to provide a light-weight framework that makes it easy to implement and explore algorithms for verifying software. The input to SvLibChecker is given in SV-LIB, an intermediate language that relieves the developers from dealing with sophisticated language features and their semantics. Software verifiers can normally be complex software systems with hundreds of thousands of lines of code. Due to the simple input, algorithms in SvLibChecker can be written in a succinct way. Our tool currently provides six different model-checking algorithms. Each algorithm consists of about 100 lines of Python code. The full project has about 2500 LOC in total, which are well-documented and have a good test coverage (> 90 %). The simplicity, lean architecture, and modular design of SvLibChecker lends itself for education. It is much easier to understand the implementation of an algorithm implemented in SvLibChecker, compared to complex verifiers for languages like C. SvLibChecker’s predicate abstraction with CEGAR has a performance comparable to CPAchecker, a mature state-of-the-art tool for software verification. The combination of simplicity and performance makes SvLibChecker a suitable tool for verification researchers and educators, for experimenting with new verification approaches and teaching students.

ABSTRACT. We present PyCHC, a solver-agnostic framework aimed at systems of constrained Horn clauses (CHC). PyCHC provides intuitive Python APIs to create and manipulate CHC systems programmatically and solve them using different backend solvers. Furthermore, PyCHC offers a certification pipeline to validate the correctness of results reported by the CHC solvers, via the use of independent satisfiability modulo theories (SMT) solvers and proof checkers. We present our framework's architecture and features, and demonstrate how it enables rapid prototyping of new CHC-based algorithms and experimentation with novel strategies for cooperative solving. We used PyCHC to validate the results of the Eldarica, Golem, and Spacer solvers on CHC-COMP benchmarks, finding several issues across different tool versions.

ABSTRACT. Quantum compiler optimization relies on rewriting rules derived from equivalences between quantum circuits, yet prior work has identified thousands of such identities, creating substantial challenges for their storage, management, and effective application. For many widely used unitary gate sets, including Clifford+T, this apparent complexity is largely redundant, raising a fundamental question: How many quantum circuit identities are actually needed to generate all others? In this work, we provide strong evidence that a small set of independent identities suffices to generate all circuit equivalences of bounded depth. Surprisingly, for circuits on up to nine qubits in which each side of an equality has depth at most ten, fewer than twenty independent identities are sufficient to derive all others, and for circuits on up to five qubits with depth at most ten, only 17 rules--each involving at most three qubits--are enough. These results enable significantly more compact and efficient rewriting systems for quantum compiler optimization and reveal underlying algebraic structure in common gate sets, showing that the vast majority of known circuit identities are consequences of a small foundational basis.

ABSTRACT. Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when specifications are given directly as automata, prior frameworks incur exponential blow-up when translating high-level set-based assertions into automata, which severely limits practicality. We introduce an extended set-based specification language and a specification-to-automata translation algorithm whose complexity is linear in the number of qubits, enabled by controlled automaton construction and qubit reordering. The resulting compact automata enable fully automatic Hoare-style verification of fixed-qubit quantum programs at previously infeasible scales, while substantially improving expressiveness without compromising efficiency.

ABSTRACT. Ensuring ancilla safety is a critical correctness requirement for quantum compilation, since ancilla qubits are routinely introduced to implement complex operations with fewer gates and reduced depth. However, formally verifying this property is computationally hard due to state-space explosion in the number of qubits, particularly for dirty ancilla, which carry unknown initial states and must be restored after use. We propose an end-to-end verification-and-repair framework that rigorously addresses both clean and dirty ancilla safety. Our core contribution is a two-step reduction strategy: we first prove that verifying an m-qubit dirty ancilla register decomposes into 2m independent clean ancilla safety checks; subsequently, we reduce each clean ancilla safety instance to an algebraic commutativity check against Pauli-Z and Pauli-X operators. This approach yields an efficient and naturally parallel verifier and enables actionable diagnosis by classifying violations into logic errors and phase errors. Leveraging this diagnosis, we further design lightweight repair routines that append local single-qubit rotations to eliminate a broad class of local ancilla faults. We implement the full pipeline in a prototype tool using a dual-backend architecture combining decision diagrams and weighted model counting, and validate it on diverse circuits ranging from arithmetic benchmarks to Grover’s algorithm. Our experiments demonstrate scalability to thousands of qubits and show that the proposed repairs effectively improve ancilla safety while preserving circuit functionality.

ABSTRACT. Matrix product states (MPS) are the standard tensor-network representation for ground states of one-dimensional quantum many-body systems, and they underpin widely used simulation tools such as DMRG. However, while quantum model checking has been developed mainly for quantum programs and communication protocols (with properties expressed along a time axis), there is still no comparable framework for systematically verifying spatial and size-dependent properties of physical many-body states, where the key parameter is the chain length. This paper takes a step toward bridging this gap. We propose Linear Chain Logic (LCL), a spatial logic designed to specify physically meaningful properties of periodic MPS families as the system size grows, such as nontriviality on rings and long-range asymptotic patterns. Our approach builds on a simple but powerful connection: every periodic MPS naturally induces a completely positive map (a quantum operation) on its virtual space, so many quantitative features of the MPS can be analyzed through the repeated application of the operation. Using this perspective, we derive an effective procedure to compute the inner products of an MPS at a given length and to support richer LCL specifications, without relying on brute-force state expansion. We then develop approximate model-checking algorithms that combine sound bounding with asymptotic structural analysis, enabling scalable reasoning about large system sizes. Experiments on representative MPS families illustrate that our method can automatically verify nontriviality and detect asymptotic spatial regimes in a way that complements traditional numerical techniques.

ABSTRACT. We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal. Our approach encodes quantum states, operations, and measurements into \uppaal timed automata with data extensions and external C++ function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol---a time-slotted generalization of superdense coding---combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

ABSTRACT. We present Quokka, a versatile, open-source Python library for quantum-circuit analysis. Quokka reduces various simulation, verification, and synthesis tasks to (maximum) weighted model counting (#SAT). It supports universal quantum circuits and a wide variety of gates. Quokka provides multiple encodings by treating circuit semantics in different algebraic bases and enables key performance tradeoffs by supporting various equivalence checking methods. Moreover, it realizes approximate analysis, where approximation is quantified via circuit fidelity, which is crucial for synthesizing circuits in different gate sets and for real-world, noisy quantum computing, where circuit depth is limited, as approximations allow for large reductions in circuit complexity. This paper demonstrates the design, extensibility, and use of Quokka.

ABSTRACT. A hard real-time system cannot miss any deadline. A weakly-hard real-time system, on the contrary, is designed to tolerate a specific number of deadline misses. For instance, the AnyMiss(2, 300) weakly-hard constraint stipulates that in every window of 300 consecutive jobs, at most 2 deadlines are missed. The weakly-hard model is the state-of-the-art for industrial dependability-by-design of control systems that tolerate deterministic failures. Weakly-hard constraints correspond to regular languages. The size of the minimal finite state machine that recognizes whether a string satisfies the constraint (about 45k states for AnyMiss(2, 300)) is a notorious impediment for the verification of control system properties. This paper discusses an over-approximation of the language that allows us to provide sound safety guarantees for control systems under deadline misses that would be out of reach using the minimal finite state machine. We present a compressed language acceptor and prove that it simulates the original finite state machine. We study language cardinality properties, and report on empirical results that show how the new acceptor can be embedded in the control design workflow, leading to verifying safety for systems for which the state-of-the-art tools do not provide answers.

ABSTRACT. The reliability of autonomous systems depends on their robustness, i.e., their ability to meet their objectives under uncertainty. In this paper, we study spatiotemporal robustness of temporal logic specifications evaluated over discrete-time signals. Existing work has proposed robust semantics that capture not only Boolean satisfiability, but also the geometric distance from unsatisfiability, corresponding to admissible spatial perturbations of a given signal. In contrast, we propose spatiotemporal robustness (STR), which captures admissible spatial and temporal perturbations jointly. This notion is particularly informative for interacting systems, such as multi-agent robotics, smart cities, and air traffic control. We define STR as a multi-objective reasoning problem, formalized via a partial order over spatial and temporal perturbations. This perspective has two key advantages: (1) STR can be interpreted as a Pareto-optimal set that characterizes all admissible spatiotemporal perturbations, and (2) STR can be computed using tools from multi-objective optimization. To navigate computational challenges, we propose robust semantics for STR that are sound in the sense of suitably under-approximating STR while being computationally tractable. Finally, we present monitoring algorithms for STR using these robust semantics. To the best of our knowledge, this is the first work to deal with robustness across multiple dimensions via multi-objective reasoning.

ABSTRACT. We consider the problem of controlling a multi-mode system w.r.t. a safety goal in the Filippov sliding-mode semantics. When the goal can be enforced, we present a symbolic algorithm that enhances the previously known solution. When the goal cannot be enforced, we compare different natural best-effort criteria, identify the most promising one, and design a symbolic algorithm that synthesizes the corresponding myopically optimal control policy. We prove that the synthesized policy enjoys a regularity property known as a tame topology.

ABSTRACT. Agents in cyber-physical systems are increasingly entrusted with safety-critical tasks. Ensuring safety of these agents often requires localizing the pose for subsequent actions. Pose estimates can, e.g., be obtained from various combinations of lidar sensors, cameras, and external services such as GPS. Crucially, in safety-critical domains, a rough estimate is insufficient to formally determine safety, i.e., guaranteeing safety even in the worst-case scenario, and external services might additionally not be trustworthy. We address this problem by presenting a certified pose estimation in 3D solely from a camera image and a well-known target geometry. This is realized by formally bounding the pose, which is computed by leveraging recent results from reachability analysis and formal neural network verification. Our experiments demonstrate that our approach efficiently and accurately localizes agents in both synthetic and real-world experiments.

ABSTRACT. We reexamine the problem of verifying Markov chains with respect to step-bounded reachability probabilities. Prevailing approaches to this problem rely on encoding the state-transition matrix using either explicit or symbolic representations. While more recent work frames the verification problem as probabilistic inference, this approach does not appear to improve scalability across the board. Our insight is to cast probabilistic model checking of Markov chains as computations over tensors. This methodology enables the use of off-the-shelf compiler toolchains for optimized execution of these tensor computations on hardware accelerators. We prove the soundness of the methodology of mapping probabilistic model checking to tensor computations. We implement our approach in a tool called Tessa. Empirical evaluation shows that Tessa easily unlocks massive speedups over state-of-the-art methods on benchmarks from the literature.

ABSTRACT. Computing optimal conditional reachability probabilities in Markov decision processes (MDPs) is tractable by a reduction to reachability probabilities. Yet, this reduction yields cycling, challenging MDPs that are often notoriously hard to solve. We present an alternative, practically efficient method to compute optimal conditional reachabilities. The new method is numerically stable, can decide the threshold problem in linear time on acyclic MDPs, and yields performance comparable to standard reachability queries. We also integrate the method in an abstraction-refinement framework to analyse millions of Markov chains at once. We demonstrate the efficacy of the new methods on benchmarks from Bayesian network analysis, probabilistic programs, and runtime monitoring and show speed-ups up to multiple orders of magnitude.

ABSTRACT. Machine Learning (ML) inference is shifting from using pre-developed static, CUDA C++, GPU kernel libraries to using MLIR-based graph compilers that perform advanced optimizations and generate custom kernels. This paradigm shift reimagines how we achieve ML inference in safety-critical domains such as automotive applications. Traditional approaches relied on qualifying static kernel libraries—pre-built for fixed input shapes and parameter ranges—according to the ISO 26262 standard. However, the demanding performance requirements of diverse ML models and rapidly evolving hardware accelerators necessitate generating optimized kernels on the fly, which only ML graph compilers can provide. This paper presents an industrial experience report on a comprehensive verification framework for ML inference in automotive applications. We describe the transition from static kernels to dynamic ML graph compilation and introduce two complementary verification strategies: (1) formal methods targeting memory safety and concurrency properties in CUDA kernels and MLIR-based compiler; and (2) AI-driven testing for functional correctness. Our experience over multiple years of production use demonstrates that validating ML graph compiler output can achieve safety assurance levels comparable to compiler qualification while enabling performance and flexibility benefits. We discuss remaining challenges including scalability of formal verification and adapting to evolving compilers and hardware platforms.

ABSTRACT. \emph{Caesar} is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative \emph{intermediate verification language} based on the real-valued logic HeyLo. HeyVL allows to express a probabilistic program, its specifications, and proof rules in a programming-language-style, so that new proof rules can be easily integrated into the verifier. Caesar translates HeyVL programs into verification conditions, which are then checked using the Z3 SMT solver. It also includes another backend based on probabilistic model checking for a subset of HeyVL. We report on the results of five years of development of Caesar, highlighting its main features and architecture. In particular, we highlight recent improvements such as additional proof rules, a model checking backend, and better diagnostics.

ABSTRACT. We present a tool for the compositional verification and correct-by-construction synthesis of stochastic world models---heterogeneous networks of interdependent stochastic models including discrete and continuous-time Markov chains, Markov decision processes (MDPs), partially observable MDPs, and stochastic multi-player games. Through its unique integration of multiple probabilistic and parametric model checking paradigms, our tool unifies the modelling, verification and synthesis of systems characterised by a combination of probabilistic and nondeterministic uncertainty, discrete and continuous-time behaviour, partial observability, and multi-agent interaction.