ABSTRACT. Atomic broadcast is a core abstraction for building fault-tolerant distributed systems, ensuring that all correct processes deliver messages in a consistent total order. The Speculative Primary-Order Atomic Broadcast (SPOabcast) protocol supports dynamic reconfiguration while maintaining message propagation through speculative delivery. This optimisation, however, introduces subtle correctness challenges. In this paper, we develop several formal models of SPOabcast using the mCRL2 process algebra and verify key correctness properties expressed in the modal $\mu$-calculus. Due to the complexity of the protocol, exhaustive verification is necessarily limited to bounded configurations. Nevertheless, the modelling and verification effort uncovers two previously unknown errors, including a subtle reconfiguration flaw that is not revealed by automated model checking alone. We propose and formally validate corrections to these errors. Our results demonstrate the value of detailed operational modelling for analysing speculative, reconfigurable broadcast protocols, and highlight the need for scalable verification techniques to address their inherent complexity.

ABSTRACT. Graham’s Scan is a classic algorithm that computes thesmallest convex polygon enclosing a set of points in the plane. Verifying a concrete implementation for Graham’s Scan, however, requires more than the textbook geometric argument: degenerate inputs, polar-angle sorting and in-place stack manipulation all affect correctness at machine level. In this paper, we present an end-to-end verification of a hand-written C implementation of Graham’s Scan against a high-level Rocq specification. The proof is structured with two layers. For abstract algorithm correctness, we decompose global geometric properties into local properties and additonally treat degenerate cases with a precise geometric setting. We then rewrite global convex-hull properties as equivalent local formulations of convexity and maximality. These properties are preserved by the incremental stack construction. For the C implementation, we use Qualified C Programming (QCP) framework to verify pivot selection, the polar-angle sorting method, array ownership, stack invariants and overflow-preventing coordinate bounds. The final refinement theorem consequently composes the verified sorting phase with the verified hull-construction loop, showing that the C program implements the abstract Rocq specification, executes with safe behavior, and returns a geometrically correct convex hull.

ABSTRACT. The rise of Arm virtualization in IoT, edge, and embedded systems makes hypervisor security verification essential. Prior hypervisor verification has established broad functional-correctness and memory-isolation properties, but has not made the bit-level behavior of dedicated AArch64 register-protection handlers a proof target. These registers govern memory translation, enforce privilege-level boundaries, and control hardware security features such as Privileged Access Never (PAN), Write implies eXecute Never (WXN), and Memory Tagging Extension (MTE), all of which malicious register writes can undermine. This paper presents an Isabelle/HOL framework for formally verifying AArch64 hypervisor register protection. Our approach builds layered Isabelle/HOL models and uses interpretation proofs to connect concrete Isabelle register-handler models to abstract security properties. We categorize security-critical Exception Level 1 (EL1) registers as either control registers or status registers, and design targeted protection strategies: bit-level monotonicity enforcement for security features and post-boot locking for translation configuration. Rigorous theorem proving verifies functional correctness and the stated security properties of the modeled protection mechanisms. Our results demonstrate that the formal state machine maintains integrity through monotonicity, consistency, and architectural well-formedness.

ABSTRACT. Craig interpolation is an important technique for modular and local reasoning in program verification. This paper studies Craig interpolation for trigonometric polynomial formulas with affine phases. For such formulas, a natural approach is to lift each trigonometric term to a fresh variable, transforming the formulas into semialgebraic ones. However, lifting trigonometric terms independently may lose relations induced by their phases and thus fail to preserve mutual inconsistency between the original formulas. We propose a unified framework to address this issue. The key idea is to rewrite all phases as integer linear combinations of phase generators before lifting, so that the relations among them are preserved. Starting from this representation, we transform the problem into a semialgebraic interpolation problem over a product of unit circles, synthesize polynomial interpolants using sum-of-squares (SOS) programming, and map them back to trigonometric ones. We establish soundness, prove completeness when the coefficient set associated with each real variable is commensurable, and prove semi-completeness under a robust separation condition otherwise. Case studies demonstrate the generation of verifiable interpolants in both regimes.

ABSTRACT. Neural language models, most notably transformers, are the backbone of today's Large Language Models (LLMs). Although such models admit fast and parallelizable training algorithms, they are often not easily amenable to analysis. In contrast, a plethora of algorithms are available for analyzing automata-based models, but such models do not admit fast training algorithms. In this talk, I will survey the growing area of FLaNN (Formal Languages and Neural Networks), which attempts to bridge these two classes of models. In particular, I will illustrate how automata theory has been used successfully to analyze various neural architectures. In addition, I will describe recent work on verifying transformer programs, which are automata-based models that capture transformers. Finally, I will discuss the challenge of producing fast and reliable code from examples using both neural language models and automata-based models.

ABSTRACT. Rely/Guarantee is a well-known verification technique for reasoning about concurrent programs. However, for some algorithms, devising suitable rely and guarantee conditions is challenging, due to the strong interference exhibited in these algorithms. The Ben-Ari concurrent garbage collector is an algorithm where the complex interactions between the components prevent the construction of compositional rely and guarantee conditions. This paper investigates an approach for verifying the Ben-Ari algorithm, which enables reasoning to be performed in a more compositional manner in cases where compositional reasoning would not otherwise be possible. This is accomplished by reasoning that a given property holds for all instances of a particular variable and then instantiating the variable to the local variable required. As well as providing a reasoning approach which is more compositional, the result is the identification of the core property required of a component, thus enabling a deeper understanding about the reasons why the algorithm works correctly. This helps to reveal the reasons why the rely/guarantee approach does not work directly for some problems.

ABSTRACT. Modern complex systems are governed by multiple behavioural requirements that vary in compatibility and context. While some properties, particularly those concerning safety and correctness, must always be enforced, others may be context-dependent or desirable only under certain conditions. Traditional runtime enforcement approaches often treat all properties uniformly, leading to enforcement conflicts.

To address this, we define the context-dependent properties, where the properties require selective enforcement. First, we define enforcement requirements and provide mechanisms to synthesize tailored enforcers that respect its enforcement goals. We examine monolithic as well as compositional approaches of enforcement. This context-dependent enforcement approach enables the system to make conflict-resolving decisions at runtime. We implement the proposed enforcers and conduct performance evaluation to assess the enforcers by analyzing execution time as the input size and the number of properties increase. Our experimentation concludes that overall, the compositional enforcers offer better scalability, whereas monolithic enforcers become increasingly unstable and often crash with more number of properties.

ABSTRACT. Abstract. Loop bound analysis is fundamental to program verification and performance analysis. Most existing techniques compute conserva- tive bounds that may considerably over-estimate actual loop iteration counts. We present a novel method for computing exact loop bounds via exit invariants. First, our method instruments loops with auxiliary vari- ables tracking initial values and loop iteration count, and computes in- variants at each exit location of the loop with the auxiliary variables. Sec- ond, our method eliminates program variables to extract exact bounds for the loop iteration counts in terms of the variables for the initial values. Third, as the bounds may be unsound, our method has a final valida- tion to ensure the soundness of our method. Experimental evaluation over representative benchmarks shows that our method is effective for deriving exact loop bounds for loops with multiple exit locations.

ABSTRACT. A classical and often-used technique in formal verification is to reduce a program analysis task to SAT and then rely on the practical efficiency of modern SAT solvers to find a solution. It is well-known that the control-flow graphs (CFGs) of structured programs are sparse and decomposable. More formally, the CFGs have bounded treewidth and pathwidth. Thus, SAT instances over these graphs can be solved by dynamic programming (DP) algorithms in worst-case linear time. Despite this, DP methods are not efficient in practice and are much slower than standard Conflict-Driven Clause Learning (CDCL), which has an exponential worst-case runtime. This leads to a natural question: Can we design a SAT-solving algorithm that exploits the sparsity of CFGs and provides both the practical efficiency of CDCL and the worst-case polynomial-time guarantee of DP?

In this work, we provide such an algorithm. We use a parameter called treedepth, which is stronger than both treewidth and pathwidth. First, we prove that the control-flow graph of a structured program has treedepth at most $2 \cdot d + 2 \cdot \lceil \lg n \rceil + 1$, where $d$ is the program's nesting depth and $n$ is the number of statements in the program. Then, we provide a novel treedepth-guided CDCL algorithm and prove that its worst-case runtime is linear in the size of the SAT instance and exponential in its treedepth. Finally, we provide an implementation of our algorithm as an extension to MiniSat, which is often used as the standard reference implementation for CDCL and CDCL-based heuristics. Our extensive experimental results show that our approach is significantly more efficient than MiniSat.

ABSTRACT. Algorithmic decision-making often relies on ranking systems to compare and prioritise alternatives. As these systems are increasingly deployed in high-stakes scenarios, the need for formal explanations of the rankings they produce has become paramount. This concern is all the more pressing given that such systems are increasingly based on machine-learning techniques, which tend to obscure the underlying decision-making process.

This paper introduces the first logical encoding for computing abductive explanations of rankings produced by machine-learning models. Specifically, we encode the problem in Answer Set Programming and use random-forest ordinal classifiers as a representative class of ranking systems. The proposed approach is implemented and evaluated on models trained using standard real-world benchmark datasets, providing evidence of the feasibility of explaining rankings, together with an analysis of performance and scalability.

ABSTRACT. Deductive verification can provide strong guarantees for heap-manipulating programs, but its practical adoption is often limited by the cost of writing formal specifications. This burden is especially pronounced in separation-logic-based verification, where specifications must precisely capture ownership, framing, aliasing, recursive predicates, and loop invariants. Although large language models (LLMs) have shown promise in specification-related synthesis tasks, it remains unclear whether they can reliably produce verifier-compatible separation logic specifications. This paper presents a systematic empirical study of LLM-generated specifications in VeriFast across C, Java, and Rust. We construct a benchmark of 148 specification-free programs derived from verified VeriFast examples and evaluate multiple LLMs using a staged verifier-based protocol that measures syntactic acceptance, type correctness, verification success, and repair-based recoverability. Our results show that LLMs often generate syntactically plausible specifications, but end-to-end full verification remains challenging due to ownership reasoning, framing, predicate construction, loop invariants, and unsound or underspecified assumptions. Verifier-guided repair recovers some failed cases, but its gains are limited and come with non-trivial token and latency overhead. Moreover, verifier-accepted specifications may still be weak or underspecified. These findings suggest that current LLMs are useful for drafting candidate specifications, but reliable VeriFast specification generation still requires stronger semantic reasoning and more robust verifier-aware synthesis methods.

ABSTRACT. Aging-related bugs (ARBs) are latent defects whose effects accumulate during long-running execution and may threaten the reliability and availability of dependable software systems. Existing ARB studies mainly operate at file level, which is useful for risk prediction but still leaves developers with coarse localization units. This paper studies function-level ARB detection as a practical warning task for dependable maintenance. We construct function-level ARB datasets for Linux, MySQL, and NetBSD by refining file-level evidence with bug reports, fixing records, patches, and evidence-based function localization. We propose MSLR-ARB, a graph learning framework that models multi-scale local views together with CFG/CDG relation-specific views. Its ARB-Oriented Self-Neighborhood Multi-Depth Encoder (ASMD Encoder) separates node-self and neighborhood transformations and retains representations from multiple propagation depths before graph-level pooling. Relation-specific representations are integrated with the local backbone for final detection. Experiments against representative generic function-level models, pre-trained code baselines, and a joint graph and sequence fusion baseline show that MSLR-ARB consistently achieves higher Balance, F1, and MCC on the studied datasets. These results suggest that combining multi-scale local structures with CFG/CDG relation-specific views provides an effective representation for function-level ARB detection in long-running software systems.

ABSTRACT. Deep reinforcement learning can generate deep neural network (DNN) controllers with good empirical control performance, but finitely many simulations cannot provide formal safety guarantees. To address the problem of infinite-horizon safe control for safety-critical systems, this paper develops a new learn-then-verify controller generation method with formal safety guarantees. The proposed method adopts a learning–abstraction–proof framework. First, a candidate DNN controller is trained using deep reinforcement learning, after which a low degree polynomial reference controller is constructed through probably approximately correct (PAC) approximation. Next, barrier certificate conditions and sum-of-squares (SOS) relaxations are used to synthesize a safe control-input interval centered at the polynomial controller, called a poly-interval model. Consequently, safety verification of the DNN controller is reduced to proving that its output is contained in this model over the entire state domain. Once this inclusion relation is established, the infinite-horizon safety guarantee of the poly-interval model is transferred to the original DNN-controlled closed-loop system. Experimental results on ten nonlinear benchmark systems show that the proposed method is applicable to DNN controllers with different network architectures and activation functions and can successfully certify systems with state dimensions of up to 12.