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.
