Identifying the actual cause of events in engineered systems is a fundamental challenge in systems. It provides a principled framework for capturing logical dependencies between events, offering insights into the underlying dynamics of a system. Finding such causes becomes more challenging in real-world systems. In this paper, we adopt the notion of probabilistic actual causality by Fenton-Glynn, which is a probabilistic extension of Halpern and Pearl’s actual causality, and propose a novel method to formally reason about causal effect of events in stochastic systems. We (1) formulate the discovery of probabilistic actual causes in computing systems as an SMT problem, and (2) address the scalability challenges by introducing an abstraction-refinement technique that improves efficiency by up to 95
PROMELA, the modeling language of SPIN, is widely used to specify and model check finite-state concurrent systems but lacks support for deductive verification. This paper presents an executable semantics of PROMELA in the 𝕂 framework that enables code-level deductive verification. To address the nontrivial interactions between guarded nondeterminism and concurrency, we introduce Load-and-Fire, an elegant semantic pattern that yields a modular, uniform treatment of guarded nondeterminism, cross-process interference, and atomicity in 𝕂 . Our semantics enables the full suite of analyses provided by 𝕂 , including deductive verification of PROMELA programs with infinite state spaces, a capability previously unavailable for PROMELA models. We illustrate the approach with a case study in deductive verification of an infinite-state concurrent system.
We mechanize a lightweight quantum logic in the Rocq proof assistant to verify Clifford+T quantum programs, particularly those with low T counts. Our tool is lightweight and automation-centric: Hoare triple validation composes simple rules, reduces all obligations to syntactic well-formedness side-conditions, and efficiently discharges those conditions. We demonstrate our tool using several case studies: a standard low-T Toffoli decomposition, graph-state generators, and the 7-qubit Steane encoder. A small empirical study on graph-state families shows near-linear growth in the number of Clifford gates and a slightly super-quadratic trend in the number of qubits, consistent with implementation overheads from list-based tensor representations, while repeated T gates on a single qubit exhibit an exponential blow-up due to additive branching. The results indicate that a rule-driven, syntax-directed approach suffices to verify low-T quantum circuits while keeping the trusted core and user-facing proofs simple.
Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines. We present a theory of forward symbolic execution for unstructured programs suitable for use in theorem provers that enables automated verification of both functional and non-functional program properties. The theory’s foundation is a set of inference rules where each member corresponds to an operation in a symbolic execution engine. The rules are designed to give control over the tradeoff between the preservation of precision and introduction of overapproximation. We instantiate our theory for BIR, a previously proposed intermediate language for binary analysis. We demonstrate how symbolic executors can be constructed for BIR with common optimizations such as pruning of infeasible symbolic states. We implemented our theory in the HOL4 theorem prover using the HolBA binary analysis library, obtaining machine-checked proofs of soundness of symbolic execution for BIR. We practically evaluated two applications of our theory: verification of functional properties of RISC-V binaries and verification of execution time bounds of programs running on the ARM Cortex-M0 processor. The evaluation shows that such verification can be automated with moderate overhead on medium-sized programs.
Safety-critical cyber physical systems usually require controllers that not only meet performance goal but also guarantee safety. However, the existing neural controller synthesis methods require a large number of data samples and gradient steps, which makes the real-time training infeasible when system dynamics vary over time. To address the challenge, we propose HyML-ASCS, a hybrid meta-learning framework for adaptive safety controller synthesis. HyML-ASCS combines model-based meta-learning, to generate task-specific embeddings that capture the patterns of safety controller synthesis tasks, with gradient-based meta-learning, to efficiently adapt to new synthesis tasks. This approach speeds up convergence, reduces the number of iterations required, and improves synthesis success rates, making HyML-ASCS a scalable and efficient solution for real-time control synthesis in dynamic environments. We evaluate HyML-ASCS on several benchmarks, demonstrating that it outperforms existing state-of-the-art methods in terms of synthesis efficiency, success rate, and scalability.
An important component of SMT solving is the theory of equality and uninterpreted functions, which is traditionally modelled in solvers via a congruence closure algorithm. Oftentimes, these algorithms are instrumented to provide machine checkable proofs when determining why two terms are equivalent. In a recent work published at FMCAD’22, Flatt et al. presented a modified congruence closure algorithm that could effectively produce demonstrably shorter proofs. This new algorithm relies on computing redundant equalities, which are not necessary to prove the equivalence between two terms but can provide shorter proofs. While promising, the modified algorithm was only considered in an equality saturation tool. In this work, we have adapted this algorithm to apply it within an SMT solver, and implemented our approach in the state-of-the-art solver cvc5. We discuss the challenges faced when integrating this algorithm into the backtracking nature of an SMT solver, and how we have addressed them. We evaluate our implementation on a large set of SMT-LIB benchmarks from multiple theories, and demonstrate how this new technique can result in smaller SMT proofs, while having only a moderate impact on runtime performance.
This paper introduces collaborative reachability games with energy constraints. In the considered arenas, agents can spend or gain energy during moves, or share it with their peers if their current position allows it. We study several variants of energy reachability games where agents move either synchronously or asynchronously, and with/without constraints on energy transfers among peers. We show that these problems have different complexities ranging from NP to EXPSPACE.
We present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externally-controlled) input can force infinite execution, independently of other trusted (e.g., controlled) variables.Our framework is a semantic generalization of Cousot and Cousot’s abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Miné’s decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. Our approach is implemented in an open-source tool and evaluated on benchmarks sourced from SV-COMP and modeled after real-world software, demonstrating practical effectiveness in verifying Termination Resilience and detecting potential Robust Non-Termination vulnerabilities.
Cellular automata (CA) are well-studied models of decentralized parallel computation, known for their ability to exhibit complex global behavior from simple local rules. While their dynamics have been widely explored through simulations, a formal treatment of CA as genuine language generators remains underdeveloped. We formalize CA-expressible languages as sets of finite words obtained by projecting the non-quiescent segments of configurations reachable by one-dimensional, deterministic, synchronous CA over bi-infinite grids. These languages are defined with respect to sets of initial configurations specified by a regular language as in regular model checking. To capture structured dynamics, we propose a glider-based generative semantics for CA. Inspired by the classical notion of gliders, we define a glider as a one-cell entity carrying a symbol in a certain velocity under well defined interaction semantics. We show that despite the regularity of the initial configurations and the locality of the transition rules, the resulting languages can exhibit non-regular and even non-context-free structure. This positions regular-initialized CA languages as a surprisingly rich computational model, with potential applications in the formal analysis of linearly ordered MAS.
Real-time automata (RTAs) can be viewed as a subclass of timed automata with only one clock that resets at each transition. In this paper, we propose a novel framework for learning deterministic RTAs (DRTAs) with minimal number of states from samples. Inspired by recent advances in learning deterministic finite automata, we introduce 3-valued Deterministic Real-Time Automata (3DRTAs) as an intermediate representation for the given sample set, thereby eliminating the redundancies present in existing approaches. Then, we solve the minimal DRTA learning problem from 3DRTAs by a reduction to a Boolean Satisfiability (SAT) problem. This then allows us to leverage state-of-the-art SAT solvers to find a minimal DRTA consistent with the given samples efficiently. More importantly, small DRTAs not only offer compact representation but also better interpretability of real-world systems. Experimental results demonstrate that our 3DRTA-based framework yields minimal DRTAs with significantly fewer states compared to those of existing methods. The proposed technique also opens new possibilities for scalable real-time automata learning in complex real-time domains.
We present our methodology to formally prove properties of VHDL designs by first translating them to Rocq. Because our translation keeps all parameters (a.k.a. generics) uninstantiated, we develop algorithms that check the correctness of given VHDL designs under all parameter valuations. These checks detect whether there are combinatorial loops, missing or multiple signal assignments, wrong integer assignments with respect to specified ranges, array access and assignment errors, and integer overflows for some valuation of the parameters. Once these checks pass, we show how to compute a topological ordering of the signal assignments that is valid for all parameter valuations, and which allows us to translate to simple Rocq functions that capture the functional behaviors of the VHDL designs given as input. We further show to address pipelined circuits and present an application on the verification of a FPU.
Quantitative verification can provide deep insights into reliable Network-On-Chip (NoC) designs. It is critical to understanding and mitigating operational issues caused by power supply noise (PSN) early in the design process: fluctuations in network traffic in modern NoC designs cause dramatic variations in power delivery across the network, leading to unreliability and errors in data transfers. Further complicating these challenges, NoC designs vary widely in size, usage, and implementation. This case study paper presents a principled, systematic, and modular NoC modeling approach using the Modest language that closely reflects the standard hierarchical design approach in digital systems. Using the Modest Toolset, functional and quantitative correctness was established for several NoC models, all of which were instantiated from a generic modular router model. Specifically, this work verifies the functional correctness of a generic router, inter-router communication, and the entire NoC. Statistical model checking was used to verify PSN-related properties for NoCs of size up to 8x8.
Sound static analysis can prove the absence of data races by establishing that no two conflicting memory accesses can occur at the same time. We repurpose the concept of digests—summaries of computational histories originally introduced to bring tunable concurrency-sensitivity to thread-modular value analysis by abstract interpretation, extending this idea to race detection: We use digests to capture the conditions under which conflicting accesses may not happen in parallel. To formalize this, we give a definition of data races in the thread-modular local trace semantics and show how exclusion criteria for potential conflicts can be expressed as digests. We report on our implementation of digest-driven data race detection in the static analyzer Goblint, and evaluate it on the Sv-Comp benchmark suite. Combining the lockset digest with digests reasoning on thread ids and thread joins increases the number of correctly solved tasks by more than a factor of five compared to lockset reasoning alone.
The widespread adoption of deep neural networks (DNNs) requires efficient techniques for verifying their safety. DNN verifiers are complex tools, which might contain bugs that could compromise their soundness and undermine the reliability of the verification process. This concern can be mitigated using proofs: artifacts that are checkable by an external and reliable proof checker, and which attest to the correctness of the verification process. However, such proofs tend to be extremely large, limiting their use in many scenarios. In this work, we address this problem by minimizing proofs of unsatisfiability produced by DNN verifiers. We present algorithms that remove facts which were learned during the verification process, but which are unnecessary for the proof itself. Conceptually, our method analyzes the dependencies among facts used to deduce UNSAT, and removes facts that did not contribute. We then further minimize the proof by eliminating remaining unnecessary dependencies, using two alternative procedures. We implemented our algorithms on top of a proof producing DNN verifier, and evaluated them across several benchmarks. Our results show that our best-performing algorithm reduces proof size by 37
Static analyzers are complex pieces of software with large dependencies. They can be difficult to install, which hinders adoption and creates barriers for students learning static analysis. This work introduces Try-Mopsa: a scaled-down version of the Mopsa static analysis platform, compiled into JavaScript to run purely as a client-side application in web browsers. Try-Mopsa provides a responsive interface that works on both desktop and mobile devices. Try-Mopsa features all the core components of Mopsa. In particular, it supports relational numerical domains. We present the interface, changes and adaptations required to have a pure JavaScript version of Mopsa. We envision Try-Mopsa as a convenient platform for onboarding or teaching purposes.
For quantum computers based on photonics, one main problem is the synthesis of a photonic circuit that emulates quantum computing gates. The problem requires using photonic components to build a circuit that act like a quantum computing gate with some probability of success. This involves not only finding a circuit that can correctly act like a quantum gate, but also optimizing the probability of success. Whilst many approaches have been given in the past and applied to specific gates, they often lack ease of reusability. We present a tool that uses dReal, a δ-weakening SMT solver, to find such photonic circuits, optimize the likelihood of occurring, and provide some guarantee that the result is optimal. We demonstrate the usage of our tool by recreating known results in the literature, extending upon them, and presenting new results for Givens rotation gates.
Previous research on the Adiar BDD package has been successful at designing algorithms capable of handling large Binary Decision Diagrams (BDDs) stored in external memory. To do so, it uses consecutive sweeps through the BDDs to resolve computations. Yet, this approach has kept algorithms for multi-variable quantification, the relational product, and variable reordering out of its scope. In this work, we address this by introducing the nested sweeping framework. Here, multiple concurrent sweeps pass information between each other to compute the result. We have implemented the framework in Adiar and used it to create a new external memory multi-variable quantification algorithm. In practice, this improves Adiar’s running time by a factor of 1.7. In turn, this work extends the previous research results on Adiar to also apply to its quantification operation: compared to conventional depth-first implementations, Adiar with nested sweeping is able to solve more problems and/or solve them faster.
Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the -calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like approach to build and refine the abstract state space with input-based splitting. This leads to a state space formalism that is much simpler than in previous TVAR frameworks, which use modal transitions. We implemented the framework in our open-source tool machine-check and verified properties of machine-code systems for the AVR architecture, showing the ability to verify systems and -calculus properties not verifiable by naïve model checking or CEGAR, respectively. This is the first practical use of TVAR for machine-code verification.
The Abstract interpretation offers sound and decidable approximations for undecidable queries related to program behavior. The effectiveness of an abstract interpretation process relies entirely on the abstract domain itself, and the worst-case scenario is when the abstract interpreter responds with "don't know", meaning that anything could happen during runtime. The concept of completeness relates to the answer precision degree when performing computations within the abstract domain. However, completeness for a whole language is an ideal domain property, usually holding only on trivial situations [20]; for this reason, a local notion of completeness, holding on a specific program input, has been deeply investigated [5]. In this paper, we characterize an intermediate notion holding for sets of input selected by abstraction. In other words, completeness holds for a set of concrete inputs determined by one abstract input. In this sense, it is a form of local abstract completeness required locally on one specific abstract value. We provide a simple proof system for proving this weakening of completeness and several examples. Notably, this proof system is both language and domain-agnostic and can be readily incorporated to support static program analysis.
Model checking trees generated by Higher-Order Recursion Schemes (HORS) of order k against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong'06). We exhibit a natural fragment of HORS, called tail-recursive HORS, and a restricted APT model, called bounded-alternation APT, such that the problem of model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT is k-1-EXPSPACE-complete. The upper bound is achieved by converting the problem into an alternating reachability game, the lower one via reduction from a tiling problem.
