title: Extending AALpy with Passive Learning: A Generalized State-Merging Approach

authors:
Benjamin von Berg
Bernhard K. Aichernig

abstract: Abstract AALpy is a well-established open-source automata learning library written in Python with a focus on active learning of systems with IO behavior. It provides a wide range of state-of-the-art algorithms for different automaton types ranging from fully deterministic to probabilistic automata. In this work, we present the recent addition of a generalized implementation of an important method from the domain of passive automata learning: state-merging in the red-blue framework. Using a common internal representation for different automaton types allows for a general and highly configurable implementation of the red-blue framework. We describe how to define and execute state-merging algorithms using AALpy, which reduces the implementation effort for state-merging algorithms mainly to the definition of compatibility criteria and scoring. This aids the implementation of both existing and novel algorithms. In particular, defining some existing state-merging algorithms from the literature with AALpy only takes a few lines of code.


venue: cav

title: Data-Driven Verification of Procedural Programs with Integer Arrays

authors:
Ahmed Bouajjani
Wael-Amine Boutglay
Peter Habermehl

abstract: Abstract We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose a new algorithmic method for synthesizing loop invariants and procedure pre/post-conditions represented as universally quantified first-order formulas constraining the array elements and program variables. We adopt a data-driven approach that extends the decision tree Horn-ICE framework to handle arrays. We provide a powerful learning technique based on reducing a complex classification problem of vectors of integer arrays to a simpler classification problem of vectors of integers . The obtained classifier is generalized to get universally quantified invariants and procedure pre/post-conditions. We have implemented our method and shown its efficiency and competitiveness w.r.t. state-of-the-art tools on a significant benchmark.


title: On the Complexity of Checking Mixed Isolation Levels for SQL Transactions

authors:
Ahmed Bouajjani
Constantin Enea
Enrique Román-Calvo

abstract: Abstract Concurrent accesses to databases are typically grouped in transactions which define units of work that should be isolated from other concurrent computations and resilient to failures. Modern databases provide different levels of isolation for transactions that correspond to different trade-offs between consistency and throughput. Quite often, an application can use transactions with different isolation levels at the same time. In this work, we investigate the problem of testing isolation level implementations in databases, i.e., checking whether a given execution composed of multiple transactions adheres to the prescribed isolation level semantics. We particularly focus on transactions formed of SQL queries and the use of multiple isolation levels at the same time. We show that many restrictions of this problem are NP-complete and provide an algorithm which is exponential-time in the worst-case, polynomial-time in relevant cases, and practically efficient.


title: Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks

authors:
Marius Bozga
Radu Iosif
Arnaud Sangnier
Neven Villani

abstract: Abstract We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars in the style of Courcelle. Due to the undecidability of verification problems such as reachability or coverability of a given configuration, in which we count the number of replicas in each local state, we develop two orthogonal verification techniques. We present a counting abstraction able to produce, from a graph grammar describing a parameterized system, a finite set of Petri nets that over-approximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evaluated on a non-trivial set of test cases. Moreover, we identify a decidable fragment, for which the coverability problem is in and -hard.


title: Automated Parameterized Verification of a Railway Protection System with Dafny

authors:
Roberto Cavada
Alessandro Cimatti
Alberto Griggio
Christian Lidström
Gianluca Redondi
Giuseppe Scaglione
Matteo Tessi
Dylan Trenti

abstract: Abstract In this paper we describe an industrial experience in the verification of the logic of a Railway Protection System (RPS). The RPS is designed within AIDA, a structured model-based design workflow and toolset. The RPS is written in a domain specific language amenable to signaling engineers, that is converted into Extended Finite State Machines (EFSM), and then into executable code. The RPS is parameterized, i.e., it can be applied, after configuration, in different operational scenarios. The logic is divided in classes, that are instantiated depending on the specific application. The verification challenge is to ensure that the required properties hold for all possible instantiations . We follow a verification approach based on the use of deductive methods, leveraging the Dafny framework. The AIDA environment is used to translate the RPS logic into Dafny, and also to automatically generate the contracts summarizing the methods implementing the guards and effects of the EFSM transitions. This approach greatly limits the need for human interaction with the underlying Dafny proof engine. In addition to domain specific optimizations, it results in an automated and efficient proof of the RPS properties.


title: sfGPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency

authors:
Soham Chakraborty
S. Krishna
Andreas Pavlogiannis
Omkar Tuppe

abstract: Abstract GPU computing is embracing weak memory concurrency for performance improvement. However, compared to CPUs, modern GPUs provide more fine-grained concurrency features such as scopes, have additional properties like divergence, and thereby follow different weak memory consistency models. These features and properties make concurrent programming on GPUs more complex and error-prone. To this end, we present $$\textsf{GPUMC}$$ GPUMC , a stateless model checker to check the correctness of GPU shared-memory concurrent programs under scoped-RC11 weak memory concurrency model. $$\textsf{GPUMC}$$ GPUMC explores all possible executions in GPU programs to reveal various errors - races, barrier divergence, and assertion violations. In addition, $$\textsf{GPUMC}$$ GPUMC also automatically repairs these errors in the appropriate cases. We evaluate $$\textsf{GPUMC}$$ GPUMC on benchmarks and real-life GPU programs. $$\textsf{GPUMC}$$ GPUMC is efficient both in time and memory in verifying large GPU programs where state-of-the-art tools are timed out. In addition, $$\textsf{GPUMC}$$ GPUMC identifies all known errors in these benchmarks compared to the state-of-the-art tools.


title: Verifying Fault-Tolerance of Quantum Error Correction Codes

authors:
Kean Chen
Yuhao Liu
Wang Fang
Jennifer Paykin
Xin-Chuan Wu
Albert T. Schmitz
Steve Zdancewic
Gushu Li

abstract: Abstract Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.


title: Compositional Abstraction for Timed Systems with Broadcast Synchronization

authors:
Hanyue Chen
Miaomiao Zhang
Frits W. Vaandrager

abstract: Abstract Simulation-based compositional abstraction effectively mitigates state space explosion in model checking, particularly for timed systems. However, existing approaches do not support broadcast synchronization, an important mechanism for modeling non-blocking one-to-many communication in multi-component systems. Consequently, they also lack a parallel composition operator that simultaneously supports broadcast synchronization, binary synchronization, shared variables, and committed locations. To address this, we propose a simulation-based compositional abstraction framework for timed systems, which supports these modeling concepts and is compatible with the popular UPPAAL model checker. Our framework is general, with the only additional restriction being that the timed automata are prohibited from updating shared variables when receiving broadcast signals. Through two case studies, our framework demonstrates superior verification efficiency compared to traditional monolithic methods.


title: Infinite-State Liveness Checking with rlive

authors:
Alessandro Cimatti
Alberto Griggio
Christopher Johannsen
Kristin Yvonne Rozier
Stefano Tonetta

abstract: Abstract is a recently-proposed SAT-based liveness model checking algorithm that showed remarkable performance compared to other state-of-the-art approaches, both in absolute terms (solving more problems overall than other engines on standard benchmark sets) as well as in relative terms (solving several problems that none of the other engines could solve). proves or disproves properties of the form FGq , by trying to show that $$\lnot q$$ ¬ q can be visited only a finite number of times via an incremental reduction to a sequence of reachability queries. A key factor in the good performance of is the extraction of “shoals” from the inductive invariants of the reachability queries to block states that can reach $$\lnot q$$ ¬ q a bounded number of times. In this paper, we generalize to handle infinite-state systems, using the Verification Modulo Theories paradigm. In contrast to the finite-state case, liveness cannot be simply reduced to finding a bound on the number of occurrences of $$\lnot q$$ ¬ q on paths. We propose therefore a solution leveraging predicate abstraction and termination techniques based on well-founded relations. In particular, we show how we can extract shoals that take into account the well-founded relations. We implemented the technique on top of the open source VMT engine IC3ia and we experimentally demonstrate how the new extension maintains the performance advantages (both absolute and relative) of the original , thus significantly contributing to advancing the state of the art of infinite-state liveness verification.


title: Structural Operational Semantics for Functional and Security Verification of Pipelined Processors

authors:
Robert J. Colvin
Roger C. Su

abstract: Abstract The design of computer microarchitectures is a challenging task, involving a trade-off between efficiency and security. In the literature, two concerns which are affected by the details of the microarchitecture – formal assembly semantics, and vulnerability discovery and mitigation – are often addressed separately. In this paper we provide a structural operational semantics for pipelined microprocessors (Arm, x86, RISC-V) that is based on a regular understanding of microarchitectural features (pipelines, branch prediction, caches, privilege checks), conforms to established memory consistency models, and exposes the Spectre and Meltdown vulnerabilities. A key point is that the operational rules correspond to stages of the pipeline and are based almost entirely on syntactic aspects of fetched instructions, as is generally understood to be the case in real pipelines. We develop a model checker based closely on the semantics, which we use to experimentally validate the model and to provide the basis for security analyses.


title: Verifying PETSc Vector Components Using CIVL

authors:
Venkata Dhavala
Jan Hückelheim
Paul D. Hovland
Stephen F. Siegel

abstract: Abstract This paper presents a modular approach to verifying the vector module of PETSc, a widely used library in scientific computing, using the CIVL model checker. Our approach relies on the creation of stub functions, which serve a dual purpose of specifying the intended behavior of individual PETSc functions and providing an abstraction for called functions to allow efficient verification of callers. This facilitates the use of symbolic execution and model checking to establish the correctness of isolated functions. Our work contributes to the ongoing effort to enhance the reliability of high-performance computing libraries and proposes an effective verification strategy for complex scientific software.


title: NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks

authors:
Hai Duong
ThanhVu Nguyen
Matthew B. Dwyer

abstract: Abstract Deep Neural Networks (DNNs) are increasingly deployed in critical applications, where ensuring their safety and robustness is paramount. We present $$_\text {CAV25}$$ CAV 25 , a high-performance DNN verification tool that uses the DPLL(T) framework and supports a wide-range of network architectures and activation functions. Since its debut in VNN-COMP’23, in which it achieved the New Participant Award and ranked 4th overall, $$_\text {CAV25}$$ CAV 25 has advanced significantly, achieving second place in VNN-COMP’24. This paper presents and evaluates the latest development of $$_\text {CAV25}$$ CAV 25 , focusing on the versatility, ease of use, and competitive performance of the tool. $$_\text {CAV25}$$ CAV 25 is available at: https://github.com/dynaroars/neuralsat .


title: Counterexample-Guided Commutativity

authors:
Marcel Ebbinghaus
Dominik Klumpp
Andreas Podelski

abstract: Abstract We consider the use of commutativity-based reduction for the algorithmic verification of concurrent programs. In existing work, the commutativity relation used for the reduction is mostly fixed statically. In this paper, we propose a demand-driven approach to compute the commutativity relation. The approach can be viewed as the direct analogue of the CEGAR approach which uses counterexamples to guide the incremental refinement of the abstraction. Instead of eliminating a counterexample by proving it infeasible and refining the abstraction, we can eliminate a counterexample by proving it redundant and expanding the commutativity relation. When we prove a counterexample redundant, we use the proof for a generalization step which allows us to eliminate not just a single counterexample, but a whole infinite set. We present a general scheme where we integrate the new approach with the CEGAR approach. We have implemented an instantiation of the general scheme. An experimental evaluation shows an increase in the number of successfully verified programs by 15% on a challenging benchmark set.


title: Fifteen Years of Viper

authors:
Marco Eilers
Malte Schwerhoff
Alexander J. Summers
Peter Müller

abstract: Abstract Viper is a verification infrastructure that facilitates the development of automated verifiers based on separation logic. Viper consists of the Viper intermediate language and two backend verifiers based on symbolic execution and verification condition generation, respectively. It has been used to build over a dozen program verifiers that translate verification problems in Go, Java, Python, Rust, and many others, into the Viper language and automate verification using the Viper backends. In this paper, we describe the original design goals for Viper’s language, verification logic, and tool architecture, summarize our experiences, and explain our principles for evolving the system.


title: Verifying Tree-Manipulating Programs via CHCs

authors:
Marco Faella
Gennaro Parlato

abstract: Abstract Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our approach is the knitted-tree encoding , modeling each program execution as a tree structure capturing input, output, and intermediate states. Leveraging the compositional nature of knitted-trees, we encode these structures as constrained Horn clauses (CHC s), reducing verification to CHC satisfiability. To illustrate our approach, we focus on memory safety and show how it naturally leads to simple, modular invariants.


title: Robust Probabilistic Bisimilarity for Labelled Markov Chains

authors:
Syyeda Zainab Fatmi
Stefan Kiefer
David Parker
Franck van Breugel

abstract: Abstract Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function, undermining its reliability in practical applications where transition probabilities are often approximations derived from experimental data. Motivated by this limitation, we introduce the notion of robust probabilistic bisimilarity for labelled Markov chains, which ensures the continuity of the probabilistic bisimilarity distance function. We also propose an efficient algorithm for computing robust probabilistic bisimilarity and show that it performs well in practice, as evidenced by our experimental results.


title: LearnLib: 10 years later

authors:
Markus Frohme
Falk Howar
Bernhard Steffen

abstract: Abstract In 2015, LearnLib, the open-source framework for active automata learning, received the prestigious CAV artifact award. This paper presents the advancements made since then, highlighting significant additions to LearnLib, including state-of-the-art algorithms, novel learning paradigms, and increasingly expressive models. Our efforts to mature and maintain LearnLib have resulted in its widespread use among researchers and practitioners alike. A key factor in its success is the achieved compositionality which allows users to effortlessly construct thousands of customized learning processes tailored to their specific requirements. This paper illustrates these features through the development of a learning process for the life-long learning of procedural systems. This development can be easily replicated and modified using the latest public release of LearnLib.


title: Introducing Certificates to the Hardware Model Checking Competition

authors:
Nils Froleyks
Emily Yu
Mathias Preiner
Armin Biere
Keijo Heljanko

abstract: Abstract Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.


title: Scaling GR(1) Synthesis via a Compositional Frameworkfor LTL Discrete Event Control

authors:
Hernán Gagliardi
Víctor A. Braberman
Sebastián Uchitel

abstract: Abstract We present a compositional approach to controller synthesis of discrete event system controllers with linear temporal logic (LTL) goals. We exploit the modular structure of the plant to be controlled, given as a set of labelled transition systems (LTS), to mitigate state explosion that monolithic approaches to synthesis are prone to. Maximally permissive safe controllers are iteratively built for subsets of the plant LTSs by solving weaker control problems. Observational synthesis equivalence is used to reduce the size of the controlled subset of the plant by abstracting away local events. The result of synthesis is also compositional, a set of controllers that when run in parallel ensure the LTL goal. We implement synthesis in the MTSA tool for an expressive subset of LTL, GR(1), and show it computes solutions to that can be up to 1000 times larger than those that the monolithic approach can solve.


title: Efficient Probabilistic Model Checking for Relational Reachability

authors:
Lina Gerlach
Tobias Winkler
Erika Ábrahám
Borzoo Bonakdarpour
Sebastian Junges

abstract: Abstract Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability properties, such as: Is there a scheduler resolving the nondeterminism such that the probability to reach an error state is above a threshold? We consider an understudied extension that relates different reachability probabilities, such as: Is there a scheduler such that two sets of states are reached with different probabilities? These questions appear naturally in the design of randomized algorithms and in various security applications. We provide a tractable algorithm for many variations of this problem, while proving computational hardness of some others. An implementation of our algorithm beats solvers for more general probabilistic hyperlogics by orders of magnitude, on the subset of their benchmarks that are within our fragment.


title: $\mathbf{{\textsc {PyCaliper}}}$: Python-Embedded Infrastructure for RTL Verification and Specification Synthesis

authors:
Adwait Godbole
Brian Huffman
Fangfei Liu
Carlos V. Rozas
Sanjit A. Seshia

abstract: Abstract We present PyCaliper : a Python-embedded framework to formulate, verify, and auto-synthesize specifications for hardware designs at the register transfer level (RTL). By being Python-embedded, PyCaliper is easy to use and benefits from object-oriented principles and Python’s rich ecosystem. Further, PyCaliper is a common platform that integrates novel research techniques such as specification synthesis and mature, industry-scale tooling, thus allowing them to benefit from each other. We discuss the system and implementation of PyCaliper and demonstrate its use in two case studies: in the first we compare a custom verification backend with a commercial tool and gain insights about the former, and in the second we demonstrate invariant synthesis for an RTL design.


title: Accelerating Automated Program Verifiers by Automatic Proof Localization

authors:
Kiran Gopinathan
Dionysios Spiliopoulos
Vikram Goyal
Peter Müller
Markus Püschel
Ilya Sergey

abstract: Abstract Automated program verifiers such as Dafny, F $$^{\star}$$ ⋆ , Verus, and Viper are now routinely used to verify real-world software. Unfortunately, the performance of the SMT solvers employed by these tools is not always able to keep up with the increasing size and complexity of verification problems, resulting in long verification times and verification failures due to time-outs. This performance degradation occurs because large SMT queries increase the search space for the SMT solver, in particular, the number of possible quantifier instantiations. Most existing attempts to mitigate this problem require substantial manual effort to reduce the size of the search space, for instance, by decomposing proofs. In this paper, we present an automatic technique to significantly improve the performance of SMT-based program proofs by drastically reducing the proof search space for each assertion, in particular, the performed quantifier instantiations. Starting from a successful verification, we automatically extract for each assertion the quantified axioms used by the SMT solver to show that the assertion is valid. Crucially, these include lurking axioms , which are logically irrelevant, but needed to trigger the instantiation of other, relevant axioms. We describe a novel proof localization algorithm that implements a semantics-preserving source-to-source translation of a program such that re-verifying an assertion in the optimized program uses only the axioms in its proof essence. This rewriting greatly reduces the possible quantifier instantiations and, thereby, the search space for the SMT solver, such that all future runs of the verifier, for instance as part of continuous integration, are substantially faster. We implemented our algorithm for the Boogie verifier and demonstrated its effectiveness on examples from Dafny and Viper. Specifically, for files with verification times over a minute, we show significant speedups of up to 100–1000 times and no slowdowns. We also provide some evidence that these improvements persist as projects evolve.


title: Verified and Optimized Implementation of Orthologic Proof Search

authors:
Simon Guilloud
Clément Pit-Claudel

abstract: Abstract We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical propositional logic in automated reasoning tools. We formalize, in the Coq proof assistant, a proof system in sequent-calculus style for orthologic. We then prove its soundness and completeness with respect to the algebraic variety of ortholattices, and we formalize a cut-elimination theorem. In doing so, we discover and fix a missing case in a previously published proof. We then implement and verify a complete proof search procedure for orthologic. A naive implementation is exponential; to obtain an optimal quadratic run time, we optimize the implementation by memoizing its results and simulating reference equality testing. We leverage the resulting correctness theorem to implement a reflective Coq tactic. We present benchmarks showing that the procedure, under various optimizations, matches its theoretical complexity. Finally, we develop a collection of tactics, including normalization with respect to orthologic and a boolean solver, which we also benchmark. We make tactics available as a standalone Coq plugin.


title: Raven: An SMT-Based Concurrency Verifier

authors:
Ekanshdeep Gupta
Nisarg Patel
Thomas Wies

abstract: Abstract This paper presents , a new intermediate verification language and deductive verification tool that provides inbuilt support for concurrency reasoning. ’s meta-theory is based on the higher-order concurrent separation logic Iris, incorporating core features such as user-definable ghost state and thread-modular reasoning via shared-state invariants. To achieve better accessibility and enable proof automation via SMT solvers, restricts Iris to its first-order fragment. The entailed loss of expressivity is mitigated by a higher-order module system that enables proof modularization and reuse. We provide an overview of the language and describe key aspects of the supported proof automation. We evaluate on a benchmark suite of verification tasks comprising linearizability and memory safety proofs for common concurrent data structures and clients as well as one larger case study. Our evaluation shows that improves over existing proof automation tools for Iris in terms of verification times and usability. Moreover, the tool significantly reduces the proof overhead compared to proofs constructed using the Iris/Rocq proof mode.


title: Decision Heuristics in MCSat

authors:
Thomas Hader
Ahmed Irfan
Stéphane Graham-Lengrand

abstract: Abstract The Model Constructing Satisfiability (MCSat) approach to Satisfiability Modulo Theories (SMT) has demonstrated strong performance when handling complex theories such as nonlinear arithmetic. Despite being in development for over a decade, there has been limited research on the heuristics utilized by MCSat solvers as in Yices2. In this paper, we discuss the decision heuristics employed in the MCSat approach of Yices2 and empirically show their significance on QF_NRA and QF_NIA benchmarks. Additionally, we propose new ideas to enhance these heuristics by leveraging theory-specific reasoning and drawing inspiration from recent advancements in SAT solvers. Our new version of the MCSat Yices2 solver not only solves more nonlinear arithmetic benchmarks than before but is also more efficient compared to other leading SMT solvers.


title: Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems

authors:
Philippe Heim
Rayna Dimitrova

abstract: Abstract The synthesis of infinite-state reactive systems from temporal logic specifications or infinite-state games has attracted significant attention in recent years, leading to the emergence of novel solving techniques. Most approaches are accompanied by an implementation showcasing their viability on an increasingly larger collection of benchmarks. Those implementations are –often simple– prototypes. Furthermore, differences in specification formalisms and formats make comparisons difficult, and writing specifications is a tedious and error-prone task. To address this, we present , a tool for specification, realizability, and synthesis of infinite-state reactive systems. comes with an expressive specification language that allows for combining infinite-state games and temporal formulas, thus encompassing the current formalisms. The realizability checking and synthesis methods implemented in build upon recently developed approaches and extend them with newly engineered efficient techniques, offering a portfolio of solving algorithms. We evaluate on an extensive set of benchmarks, demonstrating its competitiveness with the state of the art. Furthermore, provides tooling for a general high-level format designed to make specification easier for users. It also includes a compiler to a more machine-readable format that other tool developers can easily use, which we hope will lead to a broader adoption and advances in infinite-state reactive synthesis.


title: Supermartingale Certificates for Quantitative Omega-Regular Verification and Control

authors:
Thomas A. Henzinger
Kaushik Mallik
Pouya Sadeghi
Dorde Zikelic

abstract: Abstract We present the first supermartingale certificate for quantitative $$\omega $$ ω -regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability 1) $$\omega $$ ω -regular properties.We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches.


title: Charon: An Analysis Framework for Rust

authors:
Son Ho
Guillaume Boisseau
Lucas Franceschino
Yoann Prak
Aymeric Fromherz
Jonathan Protzenko

abstract: Abstract With the explosion in popularity of the Rust programming language, a wealth of tools have recently been developed to analyze, verify, and test Rust programs. Alas, the Rust ecosystem remains relatively young, meaning that every one of these tools has had to re-implement difficult, time-consuming machinery to interface with the Rust compiler and its cargo build system, to hook into the Rust compiler’s internal representation, and to expose an abstract syntax tree (AST) that is suitable for analysis rather than optimized for efficiency. We address this missing building block of the Rust ecosystem, and propose Charon, an analysis framework for Rust. Charon acts as a swiss-army knife for analyzing Rust programs, and deals with all of the tedium above, providing clients with an AST that can serve as the foundation of many analyses. We demonstrate the usefulness of Charon through a series of case studies, ranging from a Rust verification framework (Aeneas), a compiler from Rust to C (Eurydice), and a novel taint-checker for cryptographic code. To drive the point home, we also re-implement a popular existing analysis (Rudra), and show that it can be replicated by leveraging the Charon framework.


title: Automata Learning from Preference and Equivalence Queries

authors:
Eric Hsiung
Joydeep Biswas
Swarat Chaudhuri

abstract: Abstract Active automata learning from membership and equivalence queries is a foundational problem with numerous applications. We propose a novel variant of the active automata learning problem: actively learn finite automata using preference queries —i.e., queries about the relative position of two sequences in a total preorder—instead of membership queries. Our solution is Remap , a novel algorithm which leverages a symbolic observation table along with unification and constraint solving to navigate a space of symbolic hypotheses (each representing a set of automata), and uses satisfiability-solving to construct a concrete automaton (specifically a Moore machine) from a symbolic hypothesis. Remap is guaranteed to correctly infer the minimal automaton with polynomial query complexity under exact equivalence queries, and achieves PAC–identification ( $$\varepsilon $$ ε -approximate, with high probability) of the minimal automaton using sampling-based equivalence queries. Our empirical evaluations of Remap on the task of learning reward machines for two reinforcement learning domains indicate Remap scales to large automata and is effective at learning correct automata from consistent teachers, under both exact and sampling-based equivalence queries.


title: Scaling Up Proactive Enforcement

authors:
François Hublet
Leonardo Lima
David A. Basin
Srdan Krstic
Dmitriy Traytel

abstract: Abstract Runtime enforcers receive events from a system and output commands ensuring the system’s policy compliance. Proactive enforcers extend traditional (reactive) enforcers by emitting commands at any time, rather only as a response to system actions. However, proactive enforcers have so far lacked support for many useful policy features. This, along with the existing tools’ poor performance, hinders their adoption. We present a performance-optimized, proactive enforcement algorithm for a rich policy language: metric first-order temporal logic with function applications, aggregations, and bindings. We have implemented this algorithm in EnfGuard , the first proactive enforcer tool that supports the above constructs. We evaluated our tool using a novel set of six benchmarks containing both real-world and synthetic policies and logs, demonstrating that it enforces realistic policies out-of-the-box and achieves the necessary performance to be used in real-time systems.


title: Floating-Point Neural Networks are Provably Robust Universal Approximators

authors:
Geonho Hwang
Wonyeol Lee
Yeachan Park
Sejun Park
Feras Saad

abstract: Abstract The classical universal approximation (UA) theorem for neural networks establishes mild conditions under which a feedforward neural network can approximate a continuous function f with arbitrary accuracy. A recent result shows that neural networks also enjoy a more general interval universal approximation (IUA) theorem, in the sense that the abstract interpretation semantics of the network using the interval domain can approximate the direct image map of f (i.e., the result of applying f to a set of inputs) with arbitrary accuracy. These theorems, however, rest on the unrealistic assumption that the neural network computes over infinitely precise real numbers, whereas their software implementations in practice compute over finite-precision floating-point numbers. An open question is whether the IUA theorem still holds in the floating-point setting. This paper introduces the first IUA theorem for floating-point neural networks that proves their remarkable ability to perfectly capture the direct image map of any rounded target function f , showing no limits exist on their expressiveness. Our IUA theorem in the floating-point setting exhibits material differences from the real-valued setting, which reflects the fundamental distinctions between these two computational models. This theorem also implies surprising corollaries, which include (i) the existence of provably robust floating-point neural networks; and (ii) the computational completeness of the class of straight-line programs that use only floating-point additions and multiplications for the class of all floating-point programs that halt.


title: sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses

authors:
Hongjian Jiang
Anthony W. Lin
Oliver Markgraf
Philipp Rümmer
Daniel Stan

abstract: Abstract We present $$\textsf{HornStr}$$ HornStr , the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known that invariant synthesis for RMC subsumes various important verification problems, including safety verification for parameterized systems. To achieve a simple and standardized file format, we treat the invariant synthesis problem as a problem of solving Constrained Horn Clauses (CHCs) over strings. Two strategies for synthesizing invariants in terms of regular constraints are supported: (1) L* automata learning, and (2) SAT-based automata learning. $$\textsf{HornStr}$$ HornStr implements these strategies with the help of existing SMT solvers for strings, which are interfaced through SMT-LIB. $$\textsf{HornStr}$$ HornStr provides an easy-to-use interface for string solver developers to apply their techniques to verification. At the same time, it allows verification researchers to painlessly tap into the wealth of modern string solving techniques. To assess the effectiveness of $$\textsf{HornStr}$$ HornStr , we conducted a comprehensive evaluation using benchmarks derived from applications including parameterized verification and string rewriting tasks. Our experiments highlight $$\textsf{HornStr}$$ HornStr ’s capacity to effectively handle these benchmarks, e.g., as the first solver to verify the challenging MU puzzle automatically. Finally, $$\textsf{HornStr}$$ HornStr can be used to automatically generate a new class of interesting SMT-LIB 2.6 string constraint benchmarks, which might in the future be used in the SMT-COMP strings track. In particular, our experiments on the above invariant synthesis benchmarks produce more than 30000 new constraints. We also detail the performance of various integrated string solvers, providing insights into their effectiveness on our new benchmarks.


title: StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs

authors:
Yusuke Kawamoto
Kentaro Kobayashi
Kohei Suenaga

abstract: Abstract Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To mitigate this problem, we propose a tool-assisted method for formally specifying and automatically verifying the correctness of statistical programs. In this method, programmers are required to annotate the source code of the statistical programs with the requirements for these methods. Through this annotation, they are reminded to check the requirements for statistical methods, including those that cannot be formally verified, such as the distribution of the unknown true population. Our software tool automatically checks whether programmers have properly specified the requirements for the statistical methods, thereby identifying any missing requirements that need to be addressed. This tool is implemented using the Why3 platform to verify the correctness of OCaml programs that conduct statistical hypothesis testing. We demonstrate how can be used to avoid common errors in various statistical hypothesis testing programs.


title: A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs

authors:
Bram Kohlen
Maximilian Schäffeler
Mohammad Abdulaziz
Arnd Hartmanns
Peter Lammich

abstract: Abstract We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM that is based on floating-point arithmetic. We use the Isabelle/HOL proof assistant to verify convergence of our abstract definition of interval iteration and employ step-wise refinement to derive an efficient implementation in LLVM code. To that end, we extend the Isabelle Refinement Framework with support for reasoning about floating-point arithmetic and directed rounding modes. We experimentally demonstrate that the verified implementation is competitive with state-of-the-art tools for MDPs, while providing formal guarantees on the correctness of the results.


title: Space Explanations of Neural Network Classification

authors:
Faezeh Labbaf
Tomás Kolárik
Martin Blicha
Grigory Fedyukovich
Michael Wand
Natasha Sharygina

abstract: Abstract We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by state-of-the-art.


title: Panini: An Efficient and Flexible Knowledge Compiler

authors:
Yong Lai
Kuldeep S. Meel
Roland H. C. Yap

abstract: Abstract Knowledge compilation (KC) involves compiling propositional constraints into tractable target languages which in turn efficiently support multiple analyses or queries of the constraints. Solving these queries plays a crucial role in the synthesis and verification of hardware and software systems. Recently, we proposed the target language, Constrained Conjunction & Decision Diagrams (CCDD), experimentally shown to be promising for individual model counting queries. Here, we present the compiler, $$\textsf{Panini}$$ Panini , which compiles CNF into CCDD. $$\textsf{Panini}$$ Panini supports a range of queries. We present an empirical evaluation focusing on two fundamental queries, uniform sampling and (multiple) model counting, with a wide range of applications. While counting and sampling have witnessed significant performance improvements over the years, scalability still remains the primary challenge. Our evaluation over 600 instances from model counting competitions 2022–2024 show that $$\textsf{Panini}$$ Panini achieves state of art compilation by solving 322 instances, which is 183, 148, and 38 more than Dsharp, miniC2D, and D4 respectively. Secondly, on repetitive tasks, $$\textsf{Panini}$$ Panini solves 53 and 50 more instances than ExactMC and SharpSAT-TD for model counting, and 175 and 132 more instances than SPUR and KUS for uniform sampling, respectively.


title: PyEuclid: A Versatile Formal Plane Geometry System in Python

authors:
Zhaoyu Li
Hangrui Bi
Jialiang Sun
Zenan Li
Kaiyu Yang
Xujie Si

abstract: Abstract We introduce , a unified and versatile Python-based formal system for representing and reasoning about plane geometry problems. designs a new formal language that faithfully encodes geometric information, including diagrams, and integrates two complementary components to perform geometric reasoning: (1) a deductive database with an extensive set of inference rules for geometric properties, and (2) an algebraic system for solving diverse equations involving geometric quantities. By seamlessly combining these components, enables human-like reasoning and supports generating concise reasoning steps (proofs), either fully automatically or through interactive guidance. Benchmark evaluations demonstrate that outperforms existing tools, solving a broader range of problems across both proof generation and calculation tasks. Moreover, holds significant potential for educational use and integration with advanced deep learning systems.


title: Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata

authors:
Yong Li
Soumyajit Paul
Sven Schewe
Qiyi Tang

abstract: Abstract Good-for-Games (GfG) automata require that their nondeterminism can be resolved on-the-fly, while unambiguous automata guarantee that no word has more than one accepting run. These two mutually exclusive ways of restricted nondeterminism play their roles independently in Markov chain model checking (MCMC) for almost a decade but synthesising them seems hopeless: an automaton that is both GfG and unambiguous is essentially deterministic. This work breaks this perception by combining the strengths of unambiguity with the GfG co-Büchi minimisation recently proposed by Abu Radi and Kupferman. More precisely, this combination allows us to turn unambiguous automata to certain types of probabilistic automata that can be used for MCMC. The resulting automata can be exponentially smaller, and we have provided a family of automata exemplifying this state space reduction, which translates into a significant acceleration of MCMC.


title: Sprout: A Verifier for Symbolic Multiparty Protocols

authors:
Elaine Li
Felix Stutz
Thomas Wies
Damien Zufferey

abstract: Abstract We present Sprout , the first sound and complete implementability checker for symbolic multiparty protocols. Sprout supports protocols with dependent refinements on message values, loop memory, and multiparty communication with generalized, sender-driven choice. Sprout checks implementability via an optimized, sound and complete reduction to the fixpoint logic $$\mu $$ μ CLP, and uses MuVal as a backend solver for $$\mu $$ μ CLP instances. We evaluate Sprout on an extended benchmark suite of implementable and non-implementable examples, and show that Sprout outperforms its competititors in terms of expressivity and precision, and provides competitive runtime performance. Sprout additionally provides support for verifying custom functional correctness properties beyond implementability.


title: Polyregular Model Checking

authors:
Aliaume Lopez
Rafal Stefanski

abstract: Abstract We introduce a high-level language with Python-like syntax for string-to-string, polyregular, first-order definable transductions. This language features function calls, boolean variables, and nested for-loops. We devise and implement a complete decision procedure for the verification of such programs against a first-order specification. The decision procedure reduces the verification problem to the decidable first-order theory of finite words (extensively studied in automata theory), which we discharge using either complete tools specific to this theory (MONA), or to general-purpose SMT solvers (Z3, CVC5).


title: Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking

authors:
Zhengyang Lu
Po-Chun Chien
Nian-Ze Lee
Arie Gurfinkel
Vijay Ganesh

abstract: Abstract In recent years, a diverse variety of hardware model-checking tools and techniques that exhibit complementary strengths and distinct weaknesses have been proposed. This state of affairs naturally suggests the use of algorithm-selection techniques to select the right tool for a given instance. To automate this process, we present Btor2-Select , a machine learning-based algorithm-selection framework for the hardware model-checking problem described in the word-level modeling language Btor2 . The framework offers an efficient and effective machine-learning pipeline for training an algorithm selector. Btor2-Select also enables the use of the trained selector to predict the most suitable off-the-shelf model checker for a given verification task and automatically invoke it to solve the task. Evaluated on a comprehensive Btor2 benchmark suite coupled with a set of state-of-the-art model checkers, Btor2-Select trained an algorithm selector that successfully closed over 65 % of the PAR-2 performance gap between the best single tool and the idealized virtual selector. Moreover, the selector outperformed a portfolio model checker that runs three complementary verification engines in parallel. Btor2-Select offers a simple, systematic, and extensible solution to harness the complementary strengths of diverse model checkers. With its fast and highly configurable training procedure, Btor2-Select can be easily integrated with new tools and applied to various application domains.


title: Property Directed Reachability with Extended Resolution

authors:
Andrew Luka
Yakir Vizel

abstract: Abstract Property Directed Reachability ( Pdr ), also known as IC3, is a state-of-the-art model checking algorithm widely used for verifying safety properties. While Pdr is effective in finding inductive invariants, its underlying proof system, Resolution, limits its ability to construct short proofs for certain verification problems. This paper introduces PdrER , a novel generalization of Pdr that uses Extended Resolution (ER), a proof system exponentially stronger than Resolution, when constructing a proof of correctness. PdrER leverages ER to construct shorter bounded proofs of correctness, enabling it to discover more compact inductive invariants. While PdrER is based on Pdr , it includes algorithmic enhancements that had to be made in order to efficiently use ER in the context of model checking. We implemented PdrER in a new open-source verification framework and evaluated it on the Hardware Model Checking Competition benchmarks from 2019, 2020 and 2024. Our experimental evaluation demonstrates that PdrER outperforms Pdr , solving more instances in less time and uniquely solving problems that Pdr cannot solve within a given time limit. We argue that this paper represents a significant step toward making strong proof systems practically usable in model checking.


title: QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols

authors:
Yun-Rong Luo
Aman Goel
Karem A. Sakallah

abstract: Abstract We introduce , a new procedure that employs the quantified symmetric minimization algorithm from [12] to systematically derive quantified formulas that precisely capture the onset of cutoff and saturation in distributed protocols. performs symmetry-aware forward reachability to enumerate the reachable states of a finite protocol instance, and applies symmetry-preserving logic minimization to express these states as a minimum-cost finitely-quantified reachability formula. repeats this finite analysis process to derive a sequence of reachability formulas $$R_1, R_2, R_3, \cdots $$ R 1 , R 2 , R 3 , ⋯ at increasing protocol sizes. This process terminates at size k when $$R_k$$ R k is a unique solution to symmetric minimization that yields the exact set of reachable states when evaluated at size $$k+1$$ k + 1 . We define $$c:=k$$ c : = k as the cutoff size and $$R_c:=R_k$$ R c : = R k as the cutoff formula . Empirically, $$R_c$$ R c is shown to be a reachability invariant that encodes the reachable states for any protocol size. extends the finite analysis process in [12] by introducing two algorithmic enhancements: a depth-first search algorithm that enumerates the reachable states of a finite protocol by searching only for their symmetric quotient, and an extended quantification pattern inference algorithm that expresses explicit clause orbits of finite instances by logically equivalent quantified formulas. Empirical results demonstrate that, compared to the techniques used in [12], is able to analyze a larger corpus of protocols, derive more compact quantified inductive invariants, and converge at smaller cutoffs. In contrast to previous scholarship, offers a new angle for understanding the notions of cutoff and saturation of distributed protocols. In particular, it raises intriguing questions about the unexpected role of symmetric logic minimization in this much-researched area and opens new directions for further research.


title: Relational Hoare Logic for Realistically Modelled Machine Code

authors:
Denis Mazzucato
Abdalrhman Mohamed
Juneyoung Lee
Clark W. Barrett
Jim Grundy
John Harrison
Corina S. Pasareanu

abstract: Abstract Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a realistic machine model is a challenging task. Furthermore, certain security properties—such as constant-time behavior—require relational reasoning that goes beyond traditional correctness by linking multiple execution traces within a single specification. Yet, relational verification has been extensively explored at a higher level of abstraction. In this work, we introduce a Hoare-style logic that provides low-level, expressive relational verification. We demonstrate our approach on the s2n-bignum library, proving both constant-time discipline and equivalence between optimized and verification-friendly routines. Formalized in HOL Light, our results confirm the real-world applicability of relational verification in large assembly codebases.


title: lean-smt: An SMT Tactic for Discharging Proof Goals in Lean

authors:
Abdalrhman Mohamed
Tomaz Mascarenhas
Harun Khan
Haniel Barbosa
Andrew Reynolds
Yicheng Qian
Cesare Tinelli
Clark W. Barrett

abstract: Abstract Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A key aspect of Sledgehammer is the use of proof-producing SMT solvers to prove a translated proof goal and the reconstruction of the resulting proof into valid justifications for the original goal. We present lean-smt , a tactic providing this functionality in Lean. We detail how the tactic converts Lean goals into SMT problems and, more importantly, how it reconstructs SMT proofs into native Lean proofs. We evaluate the tactic on established benchmarks used to evaluate Sledgehammer’s SMT integration, with promising results. We also evaluate lean-smt as a standalone proof checker for proofs of SMT-LIB problems. We show that lean-smt offers a smaller trusted core without sacrificing too much performance.


title: On the Almost-Sure Termination of Probabilistic Counter Programs

authors:
Sergei Novozhilov
Mingqi Yang
Mingshuai Chen
Zhiyang Li
Jianwei Yin

abstract: Abstract This paper introduces k -d PCPs – the class of probabilistic counter programs with $$k \in \mathbb {N}$$ k ∈ N counter variables inducing possibly infinite-state Markov chains. We show that the universal (positive) almost-sure termination problem is undecidable for k -d PCPs in general, yet decidable for 1-d PCPs. We present an efficient decision procedure for the latter leveraging the technique of Markov chain finitization . Moreover, we identify several classes of k -d PCPs that are reducible to 1-d PCPs – thus their termination properties can be inferred automatically. Experiments demonstrate that our decision procedure can certify (positive) almost-sure termination – without resorting to invariants or supermartingales – of non-trivial probabilistic programs beyond the scope of existing tools.


title: Integer Reasoning Modulo Different Constants in SMT

authors:
Elizaveta Pertseva
Alex Ozdemir
Shankara Pailoor
Alp Bassa
Sorawee Porncharoenwase
Isil Dillig
Clark W. Barrett

abstract: Abstract This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gr bner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.


title: Veil: A Framework for Automated and Interactive Verification of Transition Systems

authors:
George Pîrlea
Vladimir Gladshtein
Elad Kinsbruner
Qiyuan Zhao
Ilya Sergey

abstract: Abstract We present , an open-source framework for automated and interactive verification of transition systems, aimed specifically at conducting machine-assisted proofs about concurrent and distributed algorithms. is implemented on top of the proof assistant. It allows one to describe a transition system and its specification in a simple imperative language, producing verification conditions in first-order logic, to be discharged automatically via a range of SMT solvers. In case automated verification fails or if the system’s description requires statements in a higher-order logic, provides an interactive verification mode, by virtue of being embedded in a general-purpose proof assistant. We have evaluated on a large set of case studies from the distributed system verification literature, showing that its automated verification performance is acceptable for practical verification tasks, while it also allows for seamless automated/interactive verification of system specifications beyond the reach of existing automated provers.


title: POPACheck: A Model Checker for Probabilistic Pushdown Automata

authors:
Francesco Pontiggia
Ezio Bartocci
Michele Chiari

abstract: Abstract We present , the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications. provides a user-friendly probabilistic modeling language with recursion that automatically translates into Probabilistic Operator Precedence Automata (pOPA). pOPA are a class of pPDA that can express all the behaviors of probabilistic programs: sampling, conditioning, recursive procedures, and nested inference queries. On pOPA, can solve reachability queries as well as qualitative and quantitative model checking queries for specifications in Linear Temporal Logic (LTL) and a fragment of Precedence Oriented Temporal Logic (POTL), a logic for context-free properties such as pre/post-conditioning.


title: A Misconception-Driven Adaptive Tutor for Linear Temporal Logic

authors:
Siddhartha Prasad
Ben Greenman
Tim Nelson
Shriram Krishnamurthi

abstract: Abstract Linear Temporal Logic (LTL) is used widely in verification, planning, and more. Unfortunately, users often struggle to learn it. To improve their learning, they need drill, instruction, and adaptation to their strengths and weaknesses. Furthermore, this should fit into whatever learning process they are already part of (such as a course). In response, we have built a misconception-based automated tutoring system. It assumes learners have a basic understanding of logic, and focuses on their understanding of LTL operators. Crucially, it takes advantage of multiple years of research (by our team, with collaborators) into misconceptions about LTL amongst both novices and experts. The tutor generates questions using these known learner misconceptions; this enables the tutor to determine which concepts learners are strong and weak on. When learners get a question wrong, they are offered immediate feedback in terms of the concrete error they made. If they consistently demonstrate similar errors, the tool offers them feedback in terms of more general misconceptions, and tailors subsequent question sets to exercise those misconceptions. The tool is hosted for free on-line, is available open source for self-hosting, and offers instructor-friendly features.


title: Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers

authors:
Yicheng Qian
Joshua Clune
Clark W. Barrett
Jeremy Avigad

abstract: Abstract Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and Isabelle, leveraging the power of ATPs. An important component of a hammer is the translation algorithm from the ITP’s logical system to the ATP’s logical system. In this paper, we propose a novel translation algorithm for ITPs based on dependent type theory. The algorithm is implemented in Lean 4 under the name Lean-auto. When combined with ATPs, Lean-auto provides general-purpose, ATP-based proof automation in Lean 4 for the first time. Soundness of the main translation procedure is guaranteed, and experimental results suggest that our algorithm is sufficiently complete to automate the proof of many problems that arise in practical uses of Lean 4. We also find that Lean-auto solves more problems than existing tools on Lean 4’s math library Mathlib4.


title: Counter Example Guided Reactive Synthesis for LTL Modulo Theories*

authors:
Andoni Rodríguez
Felipe Gorostiaga
César Sánchez

abstract: Abstract Reactive synthesis is the process of automatically generating a correct system from a given temporal specification. In this paper, we address the problem of reactive synthesis for LTL modulo theories ( $$\textrm{LTL}^{\mathcal {T}}$$ LTL T ), which extends LTL with literals from a first-order theory and allows relating the values of data across time . This logic allows describing complex dynamics both for the system and for the environment—such as a numeric variable increasing monotonically over time. The logic also allows defining relations (and not only assignment) between variables, enabling permissive shielding. We propose a sound algorithm called Counter-Example Guided Reactive Synthesis modulo theories (CEGRES), whose core is the novel concept of reactive tautology , which are valid temporal formulas that preserve the semantics of the specification but make the algorithm conclusive. Although realizability for full $$\textrm{LTL}^{\mathcal {T}} $$ LTL T is undecidable in general, we prove that CEGRES is terminating for some important theories and for arbitrary theories when specifications do not fetch data across time. We include an empirical evaluation that shows that CEGRES can solve many reactive synthesis problems of practical interest.


title: Assessing the Quality of Binomial Samplers: A Statistical Distance Framework

authors:
Uddalok Sarkar
Sourav Chakraborty
Kuldeep S. Meel

abstract: Abstract Randomized algorithms depend on accurate sampling from probability distributions, as their correctness and performance hinge on the quality of the generated samples. However, even for common distributions like Binomial, exact sampling is computationally challenging, leading standard library implementations to rely on heuristics. These heuristics, while efficient, suffer from approximation and system representation errors, causing deviations from the ideal distribution. Although seemingly minor, such deviations can accumulate in downstream applications requiring large-scale sampling, potentially undermining algorithmic guarantees. In this work, we propose statistical distance as a robust metric for analyzing the quality of Binomial samplers, quantifying deviations from the ideal distribution. We derive rigorous bounds on the statistical distance for standard implementations and demonstrate the practical utility of our framework by enhancing APSEst, a DNF model counter, with improved reliability and error guarantees. To support practical adoption, we propose an interface extension that allows users to control and monitor statistical distance via explicit input/output parameters. Our findings emphasize the critical need for thorough and systematic error analysis in sampler design. As the first work to focus exclusively on Binomial samplers, our approach lays the groundwork for extending rigorous analysis to other common distributions, opening avenues for more robust and reliable randomized algorithms.


title: Surfer - An Extensible Waveform Viewer

authors:
Frans Skarman
Lucas Klemmer
Daniel Große
Oscar Gustafsson
Kevin Laeufer

abstract: Abstract The waveform viewer is one of the most important tools in a hardware engineer’s toolbox. It is the main interface used to track down design bugs found by simulation or formal verification. In this paper, we present Surfer, a modern waveform viewer designed to integrate with the broader hardware design ecosystem. It supports translation from bit vectors to semantically meaningful values, integration with simulation and verification tools, and lays the groundwork for interactive simulation in the open-source ecosystem.


title: Engineering an Efficient Probabilistic Exact Model Counter

authors:
Mate Soos
Kuldeep S. Meel

abstract: Abstract Given a formula F , the problem of model counting, also known as #SAT, is to compute the number of satisfying assignments of F . While model counting has emerged as a crucial primitive in diverse domains from quantitative information flow analysis to neural network verification, scalability remains a fundamental challenge despite advances in both exact and approximate counting techniques. We present $$\textsf{Ganak2}$$ Ganak 2 , a novel framework that achieves substantial performance improvements through three key technical innovations: (1) refined residual formula processing incorporating SAT-specific techniques while maintaining seamless state transitions, (2) dual independent set framework maintaining distinct SAT-eligibility and decision sets, and (3) chronological backtracking specifically adapted to model counting. Our empirical evaluation on 1600 previous model counting competition instances demonstrates that $$\textsf{Ganak2}$$ Ganak 2 successfully computes counts for 1121 instances within the one hour time limit, compared to 1032 instances by the prior state of the art approach, representing an 8.7% improvement. This progress is especially remarkable considering the extensive development and refinement of model counting tools over the years, driven by yearly competitive evaluation in the field.


title: Automated Verification of Monotonic Data Structure Traversals in C

abstract: Abstract Bespoke data structure operations are common in real-world C code. We identify one common subclass, monotonic data structure traversals (MDSTs), that iterate monotonically through the structure. For example, iterates from start to end of a character array until a null byte is found, and a binary search tree iterates from the tree root towards a leaf. We describe a new automated verification tool, Shrinker , to verify MDSTs written in C. Shrinker uses a new program analysis strategy called scapegoating size descent , which is designed to take advantage of the fact that many MDSTs produce very similar traces when executed on an input (e.g., some large list) as when executed on a ‘shrunk’ version of the input (e.g., the same list but with its first element deleted). We introduce a new benchmark set containing over one hundred instances proving correctness, equivalence, and memory safety properties of dozens of MDSTs found in major C codebases including Linux, NetBSD, OpenBSD, QEMU, Git, and Musl. Shrinker significantly increases the number of monotonic string and list traversals that can be verified vs. a portfolio of state-of-the-art tools.


title: Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

authors:
Timm Spork
Christel Baier
Joost-Pieter Katoen
Sascha Klüppelholz
Jakob Piribauer

abstract: Abstract We introduce $$(\varepsilon, \delta)$$ ( ε , δ ) -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $$(\varepsilon, \delta)$$ ( ε , δ ) -bisimulation allows the use of different tolerances for the transition probabilities ( $$\varepsilon $$ ε , additive) and total exit rates ( $$\delta $$ δ , multiplicative) of states. Fundamental properties of the notion, as well as bounds on the absolute difference of time- and reward-bounded reachability probabilities for $$(\varepsilon,\delta)$$ ( ε , δ ) -bisimilar states, are established.


title: Automated Verification of Consistency in Zero-Knowledge Proof Circuits

authors:
Jon Stephens
Shankara Pailoor
Isil Dillig

abstract: Abstract Circuit languages like Circom and Gnark have become essential tools for programmable zero-knowledge cryptography, allowing developers to build privacy-preserving applications. These domain-specific languages (DSLs) encode both the computation to be verified (as a witness generator ) and the corresponding arithmetic circuits , from which the prover and verifier can be automatically generated. However, for these programs to be correct, the witness generator and the arithmetic circuit need to be mutually consistent in a certain technical sense, and inconsistencies can result in security vulnerabilities. This paper formalizes the consistency requirement for circuit DSLs and proposes the first automated technique for verifying it. We evaluate the method on hundreds of real-world circuits, demonstrating its utility for both automated verification and uncovering errors that existing tools are unable to detect.


title: The rIC3 Hardware Model Checker

authors:
Yuheng Su
Qiusong Yang
Yiwei Ci
Tianjun Bu
Ziyu Huang

abstract: Abstract In this paper, we present rIC3, an efficient bit-level hardware model checker primarily based on the IC3 algorithm. It boasts a highly efficient implementation and integrates several recently proposed optimizations, such as the specifically optimized SAT solver, dynamically adjustment of generalization strategies, and the use of predicates with internal signals, among others. As a first-time participant in the Hardware Model Checking Competition, rIC3 was independently evaluated as the best-performing tool, not only in the bit-level track but also in the word-level bit-vector track through bit-blasting. Our experiments further demonstrate significant advancements in both efficiency and scalability. rIC3 can also serve as a backend for verifying industrial RTL designs using SymbiYosys. Additionally, the source code of rIC3 is highly modular, with the IC3 algorithm module being particularly concise, making it an academic platform that is easy to modify and extend.


title: Deeply Optimizing the SAT Solver for the IC3 Algorithm

authors:
Yuheng Su
Qiusong Yang
Yiwei Ci
Yingcheng Li
Tianjun Bu
Ziyu Huang

abstract: Abstract The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relative induction. In this paper, we introduce several optimizations for the SAT solver in IC3 based on our observations of the unique characteristics of these SAT queries. By observing that SAT queries do not necessarily require decisions on all variables, we compute a subset of variables that need to be decided before each solving process while ensuring that the result remains unaffected. Additionally, noting that the overhead of binary heap operations in VSIDS is non-negligible, we replace the binary heap with buckets to achieve constant-time operations. Furthermore, we support temporary clauses without the need to allocate a new activation variable for each solving process, thereby eliminating the need to reset solvers. We developed a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations. A comprehensive evaluation highlights the performance improvements achieved by GipSAT. Specifically, the GipSAT-based IC3 demonstrates an average speedup of $$3.61$$ 3.61 times in solving time compared to the IC3 implementation based on MiniSat.


title: A Formally Verified Robustness Certifier for Neural Networks

authors:
James Tobler
Hira Taqdees Syeda
Toby Murray

abstract: Abstract Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify that the classification of an input cannot be altered by such a perturbation. Outputs that pass this test are called certified robust . However, to the authors’ knowledge, these certification functions have not yet been verified at the implementation level. We demonstrate how previous unverified implementations are exploitably unsound in certain circumstances. Moreover, they often rely on approximation-based algorithms, such as power iteration, that (perhaps surprisingly) do not guarantee soundness. To provide assurance that a given output is robust, we implemented and formally verified a certification function for globally-robust neural networks in Dafny. We describe the program, its specifications, and the important design decisions taken for its implementation and verification, as well as our experience applying it in practice.


title: StarV: A Qualitative and Quantitative Verification Tool for Learning-Enabled Systems

authors:
Hoang-Dung Tran
Sung Woo Choi
Yuntao Li
Qing Liu
Hideki Okamoto
Bardh Hoxha
Georgios Fainekos

abstract: Abstract This paper presents StarV, a new tool for verifying deep neural networks (DNNs) and learning-enabled Cyber-Physical Systems (Le-CPS) using the well-known star reachability. Distinguished from existing star-based verification tools such as NNV and NNENUM and others, StarV not only offers qualitative verification techniques using Star and ImageStar reachability analysis but is also the first tool to propose using ProbStar reachability for quantitative verification of DNNs with piecewise linear activation functions and Le-CPS. Notably, it introduces a novel ProbStar Temporal Logic formalism and associated algorithms, enabling the quantitative verification of DNNs and Le-CPS’s temporal behaviors. Additionally, StarV presents a novel SparseImageStar set representation and associated reachability algorithm that allows users to verify deep convolutional neural networks and semantic segmentation networks with more memory efficiency. StarV is evaluated in comparison with state-of-the-art in many challenging benchmarks. The experiments show that StarV outperforms existing tools in many aspects, such as timing performance, scalability, and memory consumption.


title: Regex Decision Procedures in Extended RE#

authors:
Ian Erik Varatalu
Margus Veanes
Ekaterina Zhuchko
Juhan P. Ernits

abstract: Abstract We develop decision procedures for extended regular expressions in the new $$\textbf{ERE} \texttt {\#}$$ ERE # framework that uses span semantics , utilizing the power of symbolic derivatives . We prove a normal form theorem in Lean for $$\textbf{ERE} \texttt {\#}$$ ERE # that is closed under all Boolean operations and provides the basis for the given decision procedures. The tool is evaluated on existing SMT benchmarks for regexes that shows it to be the fastest solver to date – often orders of magnitude faster than state-of-the-art – albeit specialized for the single-variable fragment of string theory.


title: FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams

authors:
Ziyuan Wang
Bin Cheng
Longxiang Yuan
Zhengfeng Ji

abstract: Abstract Applications of decision diagrams in quantum circuit analysis have been an active research area. Our work introduces FeynmanDD, a new method utilizing standard and multi-terminal decision diagrams for quantum circuit simulation and equivalence checking. Unlike previous approaches that exploit patterns in quantum states and operators, our method explores useful structures in the path integral formulation, essentially transforming the analysis into a counting problem. The method then employs efficient counting algorithms using decision diagrams as its underlying computational engine. Through comprehensive theoretical analysis and numerical experiments, we demonstrate FeynmanDD’s capabilities and limitations in quantum circuit analysis, highlighting the value of this new BDD-based approach.


title: Deductive Synthesis of Reinforcement Learning Agents for Infinite Horizon Tasks

authors:
Yuning Wang
He Zhu

abstract: Abstract We propose a deductive synthesis framework for constructing reinforcement learning (RL) agents that provably satisfy temporal reach-avoid specifications over infinite horizons. Our approach decomposes these temporal specifications into a sequence of finite-horizon subtasks, for which we synthesize individual RL policies. Using formal verification techniques, we ensure that the composition of a finite number of subtask policies guarantees satisfaction of the overall specification over infinite horizons. Experimental results on a suite of benchmarks show that our synthesized agents outperform standard RL methods in both task performance and compliance with safety and temporal requirements.


title: ModelVerification.jl: A Comprehensive Toolbox for Formally Verifying Deep Neural Networks

authors:
Tianhao Wei
Hanjiang Hu
Luca Marzari
Kai S. Yun
Peizhi Niu
Xusheng Luo
Changliu Liu

abstract: Abstract Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained framework that allows a complete range of various model architecture and input-output properties. To this end, we present ( https://github.com/intelligent-control-lab/ModelVerification.jl ), the first comprehensive, cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying different types of DNNs and input-output specifications. This versatile toolbox is designed to empower developers and machine learning practitioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.


title: Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications

authors:
Samuel Williams
Jyotirmoy Deshmukh

abstract: Abstract Automatically constructing smooth paths that satisfy a formal specification is a challenging problem. Existing methods struggle to scale to long horizon specifications and challenging environments. We present a method that uses abstraction, model checking, and convex optimization to solve for a smooth Bézier spline that is guaranteed to satisfy a Linear Temporal Logic specification. Our approach uses a coarse abstraction to avoid the state explosion of other abstraction based methods, and successfully avoids the computational challenges of directly optimizing the non-convex temporal logic semantics. We prove our method is sound and complete and demonstrate a significant computational advantage relative to state of the art approaches. Generating such smooth paths has natural applications in path planning for autonomous robots, and we demonstrate the applicability of our method on path planning for a quadrotor.


title: Arithmetizing Shape Analysis

authors:
Sebastian Wolff
Ekanshdeep Gupta
Zafer Esen
Hossein Hojjat
Philipp Rümmer
Thomas Wies

abstract: Abstract Memory safety is a fundamental correctness property of software. For programs that manipulate linked, heap-allocated data structures, ensuring memory safety requires analyzing their possible shapes. Despite significant advances in shape analysis, existing techniques rely on hand-crafted domains tailored to specific data structures, making them difficult to generalize and extend. This paper presents a novel approach that reduces memory-safety proofs to the verification of heap-less imperative programs, enabling the use of off-the-shelf software verification tools. We achieve this reduction through two complementary program instrumentation techniques: space invariants, which enable symbolic reasoning about unbounded heaps, and flow abstraction, which encodes global heap properties as local flow equations. The approach effectively verifies memory safety across a broad range of programs, including concurrent lists and trees that lie beyond the reach of existing shape analysis tools.


title: D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation

authors:
Yingte Xu
Li Zhou
Gilles Barthe

abstract: Abstract Labelled Dirac notation is a formalism commonly used by physicists to represent many-body quantum systems and by computer scientists to assert properties of quantum programs. It is supported by a rich equational theory for proving equality between expressions in the language. These proofs are typically carried on pen-and-paper, and can be exceedingly long and error-prone. We introduce D-Hammer, the first tool to support automated equational proof for labelled Dirac notation. The salient features of D-Hammer include: an expressive, higher-order, dependently-typed language for labelled Dirac notation; an efficient normalization algorithm; and an optimized ++ implementation. We evaluate the implementation on representative examples from both plain and labelled Dirac notation. In the case of plain Dirac notation, we show that our implementation significantly outperforms DiracDec (Xu et al., POPL’25).


title: Automatic Verification of Floating-Point Accumulation Networks

authors:
David Kai Zhang
Alex Aiken

abstract: Abstract Floating-point accumulation networks (FPANs) are key building blocks used in many floating-point algorithms, including compensated summation and double-double arithmetic. FPANs are notoriously difficult to analyze, and algorithms using FPANs are often published without rigorous correctness proofs. In fact, on at least one occasion, a published error bound for a widely used FPAN was later found to be incorrect. In this paper, we present an automatic procedure that produces computer-verified proofs of several FPAN correctness properties, including error bounds that are tight to the nearest bit. Our approach is underpinned by a novel floating-point abstraction that models the sign, exponent, and number of leading and trailing zeros and ones in the mantissa of each number flowing through an FPAN. We also present a new FPAN for double-double addition that is faster and more accurate than the previous best known algorithm.


title: On the Verification Problem of Remote Direct Memory Access Programs

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Govind Rajanbabu
Stephan Spengler

abstract: Abstract Remote Direct Memory Access (RDMA) is a technology that allows direct memory access from the memory of one computer into that of another without involving either one’s operating system. This enables high-throughput, low-latency networking, which is especially useful in massively parallel computer clusters. In this paper, we study the reachability and robustness problems for RDMA programs. We show that reachability is undecidable in general, even for a restricted fragment of the model. We then focus on robustness, which asks whether a program exhibits the same behaviours under the RDMA and sequential consistency (SC) semantics, and prove that this problem is decidable. Our central technical result establishes a normal form for robustness violations, showing that any non-robust program admits a violating execution of a specific form. We then leverage this normal form to obtain a decision procedure that reduces robustness to reachability in finite-state programs with counters, yielding an ExpSpace upper bound in the general case, and a PSpace upper bound in the absence of poll operations. Finally, we also show that both of these bounds are optimal.


title: Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions

authors:
S. Akshay
Supratik Chakraborty
Soroush Farokhnia
Amir Goharshady
Harshit Jitendra Motwani
Dorde Zikelic

abstract: Abstract We present a parallel abstract interpretation technique for polynomial programs with assertions presented as unions of range bound constraints. We use the powerset domain of hyper-rectangles to over-approximate sets of reachable states. Our key technical contributions include novel abstract transformers and refinement operators that account for the semantics of polynomial assignments and guards more precisely than earlier work, while remaining amenable to parallelization and efficient implementation. This is achieved by appealing to Farkas’ Lemma and Handelman’s Theorem, and by exploiting geometric properties of unions of hyper-rectangles. Our abstract interpretation technique proves safety properties of many polynomial programs that state-of-the-art abstract interpretation tools fail to prove. We have implemented our approach in a tool called PolyAbs , and experimentally evaluated it on a suite of benchmarks. Our experiments demonstrate the improved precision and broader coverage of PolyAbs vis-a-vis state-of-the-art abstract interpretation tools, including a commercial-grade tool.


title: The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq

authors:
Andrei Aleksandrov
Malte Jackisch
Kim Völlinger

abstract: Abstract Research on neural network verification has traditionally emphasized scalability. However, recent invalidations of formally verified results of neural networks highlight soundness as an equally important goal. Pursuing inherent soundness, we present Rocq-NN-Roll , the first formally verified prover for rational-valued piecewise-affine neural networks. Rocq-NN-Roll combines a network and its specification, including hyperproperties, into a piecewise-affine function and reduces the verification task to solving linear inequalities over the network’s polyhedral regions. Developed in Rocq, the prover also provides the first automated proof support for neural networks within any interactive theorem prover, highlighting their still underexplored role in this field.


title: Kofola 1.0: A Modular Approach to ømega-Regular Complementation and Inclusion Checking

authors:
Ondrej Alexaj
Vojtech Havlena
Lukás Holík
Ondrej Lengál
Yong Li
Nicolas Mazzocchi

abstract: Abstract We present Kofola , an efficient tool for complementation and inclusion checking of Büchi automata, two central tasks in automata-theoretic verification with applications in model checking, monitoring, and theorem proving. Kofola implements a state-of-the-art modular complementation framework that decomposes the input automaton into strongly connected components and applies to each component a complementation algorithm tailored to its structural properties. Building on this modular construction, Kofola also provides modular inclusion checking with new heuristics. A key ingredient is a new on-the-fly emptiness-checking algorithm for the simple generalized Rabin pair condition produced by our complementation, allowing the search to terminate as soon as the explored state space suffices. Empirical evaluation shows that Kofola is highly competitive with state-of-the-art complementation and inclusion-checking tools: it is the most robust tool in our evaluation and often outperforms competitors by several orders of magnitude on benchmarks from practical applications.


title: A Neurosymbolic Approach to Natural Language Formalization and Verification

authors:
Chenyang An
Sam Bayless
Stefano Buliani
Darion Cassel
Byron Cook
Duncan Clough
Rémi Delmas
Nafi Diallo
Ferhat Erata
Nick Feng
Dimitra Giannakopoulou
Aman Goel
Aditya Gokhale
Joe Hendrix
Victor Heorhiadi
Marc Hudak
Dejan Jovanovic
Andrew M. Kent
Benjamin Kiesl-Reiter
Jeffrey J. Kuna
Nadia Labai
Joseph Lilien
Divya Raghunathan
Zvonimir Rakamaric
Niloofar Razavi
Michael Tautschnig
Ali Torkamani
Nathaniel Weir
Michael W. Whalen
Jianan Yao

abstract: Abstract Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc) : a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. ARc performs multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.


title: Decoupled Planning for Multiple Omega-Regular Objectives

authors:
Guy Avni
Thomas A. Henzinger
Kaushik Mallik
Suman Sadhukhan
K. S. Thejaswini

abstract: Abstract We study the problem of generating paths on a graph that satisfy a collection of $$\omega $$ ω -regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions —simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of $$\omega $$ ω -regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.


title: sweap: Reactive Synthesis for Infinite-State Integer Problems

authors:
Shaun Azzopardi
Luca Di Stefano
Nir Piterman

abstract: Abstract Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present , a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems. supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the tool, and our own bespoke input. We present a mature version of with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that outperforms its only competitor in this domain.


title: PyCHC: A Framework for Certified Horn Solving and CHC-Based Design

authors:
Anna Becchi
Martin Blicha
Rodrigo Otoni
Natasha Sharygina

abstract: 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 Z3-Spacer solvers on CHC-COMP benchmarks, finding several issues across different tool versions.


title: Best-Effort Safety Control of Multi-mode Systems

authors:
Massimo Benerecetti
Marco Faella
Fabio Mogavero

abstract: Abstract We consider the problem of controlling a multi-mode system with respect to 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 .


title: Transition Invariants Revisited: Termination Witnesses and Their Validation

authors:
Dirk Beyer
Marek Jankola
Marian Lingsch Rosenfeld

abstract: Abstract Whenever automatic software verifiers determine that a program fulfills or violates its specification, they are expected to produce also a witness that justifies the verdict. This allows a third party to independently validate the verdict and the arguments from which it was derived, increasing trust in the results. The current standard exchange format for witnesses in software verification does not support program termination. To fill this gap, we propose an extension of the witness format that is based on transition invariants as a general and effective formalism. We justify this by (a) proving that transition invariants can encode other popular termination arguments, such as ranking functions, and (b) providing three different validation approaches for transition invariants, which together can validate most of the produced witnesses. Our approach based on transition invariants was integrated into version 2.1 of the exchange format for verification witnesses, our experiments show that the new witnesses can be effectively validated and that validation is often more efficient than verification, and the software-verification community has adopted the format already for SV-COMP 2026.


title: SvLibChecker: A Light-Weight Tool for Software Model Checking

authors:
Dirk Beyer
Marian Lingsch Rosenfeld

abstract: Abstract SvLibChecker is a small tool for software model checking. Its goal is to provide a light-weight framework that makes it easy to implement and explore algorithms for software verification. The input to SvLibChecker is an SV-LIB program. SV-LIB is an intermediate language that relieves the developers from dealing with sophisticated language features and their semantics. Software verifiers are usually 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. SvLibChecker 1.0 provides nine different model-checking algorithms. Each algorithm consists of about 100 lines of Python code. The full project has 3 849LOC in total, which are well-documented and have a good code coverage (> 90 %). The simplicity, lean architecture, and modular design of SvLibChecker lends itself to 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 implementations of the algorithms show performance characteristics similar 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 rapidly experimenting with new verification approaches, and for learning and understanding how model-checking algorithms work.


title: Lagrangian-Based Duality for Quantified SMT Algorithms

authors:
Ivana Bocevska
Takeshi Tsukada
Hiroshi Unno
Oded Padon
Sharon Shoham

abstract: 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—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.


title: The Simulator's Blueprint: Automata Learning from Cybersecurity Logs

authors:
Tudor Braicu
Benjamin Ylvisaker
Nicolas A. Espinosa Dice
Yiding Chen
Yiyi Zhang
Nate Foster
Hossein Hojjat

abstract: 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 algorithms such as RPNI to infer compact 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.