Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution (e.g., scheduling, runtime environments) of stateless functions. Recently, domain-specific languages like APP and aAPP have been developed to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. Reachability analysis of FaaS scheduling policies is fundamental to check quality-of-service properties, like preventing the scheduling of functions on workers which cannot sustain expected performance levels, or verifying security properties, e.g., that safety-critical functions cannot run on nodes with untrusted ones. We investigate the complexity of reachability analysis for APP and aAPP– the latter extends APP with constraints for placing functions according to the absence/presence of other (anti-)affine functions on workers. We show that reachability analysis has linear time complexity in APP, while the addition of affinities (in aAPP) makes reachability PSPACE. Given the computational complexity correspondence between reachability analysis in aAPP and automatic planning problems (both are in PSPACE), we investigate the exploitability of planners, i.e., tools specialised for solving planning problems for the realisation of static analysers of reachability-like problems for aAPP.
This paper presents a case study in the design and formal verification of a safe controller for the generic two-element lumped-capacitance model of temperature regulation, using formal cyber-physical system (CPS) theorem proving. The coupled dynamics and the absence of a fallback state reflect the complexities of real-world control systems and make it a representative challenge for theorem proving. A controller is developed by a design-by-invariant methodology. Verification using the axiomatic theorem prover KeYmaera X revealed critical assumptions for safety and pushes the frontier of CPS theorem proving. The parametric, general and provably safe controller can be applied to a wide range of temperature regulation tasks and is validated by deploying an instance of the verified controller on a physical system, demonstrating its robustness under model inaccuracies and confirming its real-world usability.
Message parsing represents a complex security-critical problem. It has been demonstrated by numerous real-world exploits on parsers, e.g. on PKCS#1 (Public-Key Cryptography Standard) v1.5 signature, X.509 certificate chain, or infamously on a TLS extension during the Heartbleed attack. In this case study, we perform formal verification of a PKCS#1 v1.5 signature parser using Frama-C, where the verification of the parser is realized for the first time directly over the actual implementation in C. This brings highest guarantees of security and functional properties, while leaving developers the flexibility to adapt the code to the project’s specific requirements. We present the proven properties, our verification approach and results. In particular, this work rules out applications of any variants of Bleichenbacher’s signature forgery and ensures that we are able to detect potential parser incompatibilities. This work opens the door to future extensions to other protocols, for example, for parsing DER ASN.1 encoding of X.509 certificates and CRLs (Certificate Revocation Lists).
We present an approach to theory exploration, i.e., a lemma synthesis procedure which discovers algebraic laws over recursive functions over Algebraic Data Types (ADTs). The approach, LemmaCalc, builds on, adapts and extends program calculation techniques known from optimization of functional programs (fusion and accumulator removal). Our approach avoids exponential search space of term enumeration (SyGuS) that can render state-of-the-art techniques prohibitively expensive or even useless on large theories with more than a handful of function symbols. In this paper we describe how this approach can be realized and contribute a robust implementation. The evaluation shows that different methods have complementary strengths and that each can produce lemmas not found by the other, but LemmaCalc scales much better to larger theories.
We introduce the notion of a distributed timed scenario (DTS) and define the semantics of a DTS as a set of distributed behaviours. We define the notion of consistency of a DTS in terms of its semantics and develop a constructive method for determining the consistency. We define the semantic equivalence of two distributed scenarios and develop two different, but related, canonical representations for an equivalence class of distributed scenarios. Equipped with these results we tackle the problem of realisability of sets of sequential scenarios as distributed scenarios. We develop an algorithm that determines whether a set of sequential scenarios can be realised by a DTS, i.e., whether there is a DTS whose semantics is identical to the union of the behaviours allowed by the members of the set. If so, we produce such a DTS.
Cyber attacks on Industrial Control Systems (ICSs) are becoming increasingly sophisticated, undermining the ability of these systems to manage critical processes and compromising the availability of key public infrastructure. Detecting system anomalies is an important element in the identification of cyber attacks, allowing the rapid deployment of crucial incident-response activities. In this paper, we introduce a novel anomaly detection approach that integrates SPIN model checking into ICS environments to detect anomalies in live system data. Our approach uses the application code extracted from Programmable Logic Controllers (PLCs) to generate the dynamic system model, requiring only a small amount of test data to validate their design. We evaluate our approach by generating models using a representative physical hydroelectric dam testbed containing real PLCs. These models are used to analyse synthetic data containing potential irregularities that could occur within the dam as a result of false data injection attacks. Our approach was shown to identify anomalies and verify normal system behaviour. Our evaluation shows that the models achieved high performance while maintaining explainability and delivering metrics of 99.99
The behavioral specifications of a system are often partial at early stages of development due to pending design decisions. We view such specifications as being parameterized by these decisions and consider the problem of identifying a possible concretization, i.e., taking a subset of these decisions, to ensure that the system conforms to the desired requirements. We capture such a partially specified system as a partially-labeled Kripke structure ( ), where certain propositions labeling the states of the Kripke structure correspond to pending design decisions, thus may be unknown. We then reduce the verification problem to model checking different instances, each corresponding to a specific set of design decisions taken, inducing a semi-lattice on the instances. Central to our solution strategy is the effective and efficient exploration of this semi-lattice and the application of model checking techniques to s with 3-valued semantics of temporal properties, to take into account unknown state labels. We also address the problem of identifying an optimal instance of a partially-specified system that satisfies a desired property, where the cost of design decisions drive the optimality criterion. We use a prototype implementation of our strategy to validate its viability on a multi-objective path planning problem.
Modern reachability analysis techniques are highly effective when applied to software safety verification. However, they still struggle with certain classes of problems, particularly the verification of programs with complex control flow and deep nested loops. In this paper, we introduce Cycle Summarization-based Reachability Analysis (CSRA), a new Constrained Horn Clause (CHC) based approach for reachability analysis of nested-loop software. Our technique relies on the generation and refinement of cycle summaries within the CHC system. CSRA analyzes cycles in a modular manner, constructing summaries and cycle unrollings. Cycle summaries in our approach are used both to prove safety and detect potential safety violations. This enables more efficient exploration of nested loops. The prototype of CSRA is implemented within the Golem CHC solver. An empirical comparison with other reachability analysis techniques demonstrates that our approach is highly competitive in both proving safety and constructing counterexamples.
Trust modeling is critical for the safe deployment of autonomous systems, yet existing approaches that rely primarily on historical performance data fail to capture dynamic operational contexts and real-time agent capabilities. This paper introduces a formal framework for modeling actual trust in Autonomous Delivery Vehicles (ADVs)—a context-aware trust model that evaluates an agent’s current ability, knowledge state, and commitment to task completion rather than relying solely on past behavior. We present a systematic refinement-based approach using Event-B formal methods to model trust in ADV task delegation scenarios. Our methodology progresses through five refinement levels, transitioning from an untrusted baseline model to a comprehensive trust framework that integrates three key dimensions: (1) strategic trust (capability verification), (2) epistemic trust (knowledge-based assessment), and (3) commitment trust (availability and willingness evaluation). Each refinement level addresses specific failure modes identified in traditional delegation systems where tasks may be assigned to incapable, unknown, or unavailable vehicles. The formal model is verified using the Rodin theorem prover with 93 proof obligations, achieving 90
Payment channel networks such as the Lightning Network are an approach to improve the scalability of blockchain-based cryptocurrencies. The complexity of Lightning, the Lightning Network’s protocol, makes it hard to assess whether the protocol is secure. To enable computer-aided security verification of Lightning, we formalize the protocol in TLA+ and formally specify the security property that honest users are guaranteed to retrieve their correct balance. Model checking provides a fully automated verification of the security property, however, the state space of the protocol’s specification is so large that model checking is unfeasible. We make model checking of Lightning possible using two refinement steps that we verify using proofs. In a first step, we abstract the model of time and in a second step we use compositional reasoning to separately model check a single payment channel and multi-hop payments. These refinements reduce the state space sufficiently to allow for model checking Lightning with small finite models. Our results indicate that the current specification of Lightning is secure.
The increasing complexity of safety-critical systems in domains like aerospace, robotics, and industrial control demands precise modeling and verification methods. While Timed Automata (TA) and Distributed Timed Automata (DTA) are standard formalisms for real-time systems, they assume synchronized clocks or lack the expressiveness to capture clock drift and indirect timing dependencies. To overcome these limits, we propose Timed Automata with Clock Derivatives (idTA), extending TA with rate constraints to model independent clock evolution. We also introduce _ν , a temporal logic over Multi-Timed Labeled Transition Systems (MLTS), capturing properties of systems with unsynchronized clocks. We show that model checking for _ν is EXPTIME-complete. Finally, we present MIMETIC, a model checking tool supporting idTA and _ν , providing a platform for analyzing clock interactions and verification of Distributed Real-time Systems (DRTS).
Non-volatile memory (NVM) is a high-performance memory technology that supports persistency (i.e., durability) of data in case of a system crash (e.g., power failure). For implementations of concurrent objects (e.g., concurrent data structures such as stacks and hash maps), NVM poses a correctness problem: can the implementation recover to a consistent state after a crash and continue execution? In this paper, we study a notion of correctness known as buffered durable linearizability for implementations of periodically persistent concurrent objects, and develop a refinement-based proof method for buffered durable linearizability. To support our proofs, we develop a generic abstract specification of a buffered durable linearizable object that is generated from the object’s sequential specification. Our main case study is a concurrent hash map known as Dalí, which we show satisfies buffered durable linearizability. Specifically, we use FDR, a model checker based on CSP, that offers a fully automatic method for checking trace refinement.
Formal logics are central to the specification and verification of computational systems, yet their adoption outside highly specialised domains is hindered by steep learning curves and error-prone textual notations. Making these notations more approachable is particularly important in education and in settings where non-expert stakeholders need to engage with formal reasoning. We present a framework that automatically generates block-based visual editors for formal logics using the Blockly library. From a structured JSON specification of syntax and composition rules, our tool produces browser-based editors in which formulas are constructed by combining graphical blocks rather than writing code. This approach lowers syntactic barriers for learners and non-experts, while allowing experts to define new logics without manual interface design. Although integration with verification backends is planned, the tool already provides a reusable foundation for accessible and customisable logic editors.
Reasoning about incentives in a blockchain protocol can be captured by game-theoretic modeling. We present modeling principles sufficient to create a faithful representation of a blockchain protocol as an extensive form game. Such games are then suitable for automatically establishing game-theoretic security. We showcase the semi-automated generation of the game models for two parts of Bitcoin’s Lightning protocol: the closing of a channel and the routing of a payment along channels. Additionally, we provide a domain-specific language, which eases the implementation of the games. We believe our modeling principles and guidelines strengthen machine-supported modeling practices.
Race conditions in Software-Defined Networks (SDNs) pose a significant threat to the correctness and reliability of network behavior, particularly in dynamic and distributed control plane environments. This paper presents a formal approach to identifying and analyzing races in SDNs using vector clocks and DyNetKAT, a domain-specific language for specifying and reasoning about dynamic packet-processing policies. By modeling network execution traces with vector clocks, we detect concurrent events through incomparable clock states, which signal potential races. We then assess the harmfulness of these races by comparing the DyNetKAT expressions associated with the corresponding transitions, determining if the race affects the network’s behaviour. Our methodology enables systematic detection of harmful races that lead to packet drops, policy violations, or inconsistent forwarding behaviors. Through case studies and experimental validation on real network topologies, we demonstrate the effectiveness of our approach in uncovering subtle concurrency bugs that are often missed by traditional testing. This work provides a foundation for more robust SDN verification tools and contributes to the safe evolution of programmable network infrastructures.
In this paper, we use a novel combination of probabilistic programming and flowpipe construction to predict bounds on future biogas production for a wastewater treatment plant given operational data from the past. The operation of the anaerobic digester of a wastewater treatment plant is modeled through an Ordinary Differential Equation (ODE) model with unknown parameters and unobservable internal states. We are given data from the plant’s operation that includes the daily measurement of the incoming waste volumes and concentrations along with the volume of biogas produced. We formalize our problem as first estimating the unknown parameters and initial conditions using Bayesian inference, such that the past behavior of the system is “compatible” with the observed data. Next, we propagate those input parameter estimates forward using flowpipe construction. To enable rapid and accurate flowpipe construction, we exploit the monotonicity property of the dynamical model of the plant. The procedure yields an over-approximation of the upper and lower bounds on biogas production, given the inputs. As a result, it can be used to formally bound future predictions that might inform facility operations. We implemented this procedure using a first-order kinetics model of hydrolysis to model the anaerobic digester of a real-world case study facility. We demonstrate how this method constructs realistic bounds for biogas prediction from the historical data that contain the actual ground-truth data 100
We address the verification of abstract data types (ADTs) implementing associative containers like maps and sets with fine-grained specifications for iterators, which allow for multiple readers and writers in client code. Our verified implementations are written in the verification-aware programming language Dafny. In this paper we introduce new methodological contributions in verifying heap-allocated data structures, such as separation between heap-based components and functional behavior, and fine-grained control of verification proofs. Additionally, we have implemented a library of associative containers in Dafny, including a verified implementation of threaded red-black trees with iterators. These contributions aim to reduce proof complexity in order to improve verification times, while maintaining proper encapsulation.
We propose a method for combining Harmonic Control Lyapunov-Barrier Functions (HCLBFs) derived from Signal Temporal Logic (STL) specifications with any given robot policy to turn an unsafe policy into a safe one with formal guarantees. The two components are combined via HCLBF-derived safety certificates, thus producing commands that preserve both safety and task-driven behavior. We demonstrate with a simple proof-of-concept implementation for an object-centric force-based policy trained through reinforcement learning for a movement task of a stationary robot arm that is able to avoid colliding with obstacles on a table top after combining the policy with the safety constraints. The proposed method can be generalized to more complex specifications and dynamic task settings.
Hybrid systems are increasingly used in critical applications such as medical devices, infrastructure systems, and autonomous vehicles. Lince is an academic tool for specifying and simulating such systems using a C-like language with differential equations. This paper presents recent experiments that enhance Lince with mechanisms for executing multiple simulation variants and generating histograms that quantify the frequency with which a given property holds. We illustrate our extended Lince using variations of an adaptive cruise control system.
Assuring the safety and trustworthiness of autonomous systems is particularly difficult when learning-enabled components and open environments are involved. Formal methods provide strong guarantees but depend on complete models and static assumptions. Runtime verification (RV) complements them by monitoring executions at run time and, in its predictive variants, by anticipating potential violations. Large language models (LLMs), meanwhile, excel at translating natural language into formal artefacts and recognising patterns in data, yet they remain error-prone and lack formal guarantees. This vision paper argues for a symbiotic integration of RV and LLMs. RV can serve as a guardrail for LLM-driven autonomy, while LLMs can extend RV by assisting specification capture, supporting anticipatory reasoning, and helping to handle uncertainty. We outline how this mutual reinforcement differs from existing surveys and roadmaps, discuss challenges and certification implications, and identify future research directions towards dependable autonomy.
