Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification’s reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28
This paper presents a compositional approach to modelbased test derivation in Behavior-Driven Development (BDD). In BDD, system behavior is specified through scenarios written in natural language. For each scenario, a test case can be derived. However, such test cases do not cover the integration of multiple behaviors, while that is where potential faults may very well occur. To counter this, we introduce a formal composition operator for sequential composition, which integrates the individual BDDs while preserving their test coverage. We also report on a prototype tool that integrates model-based features into an existing testing framework that supports BDD-based test derivation. We show the feasibility and advantages of our approach by applying the prototype to a real-world case study.
Secure multiparty computation (hereafter, SMC) refers to cryptographic protocols that allow multiple parties to jointly compute a function over their inputs while keeping them private. The main security property of SMC protocols is information leakage freedom, whose proofs can be found in the scientific literature for idealized models. But how does one guarantee that information leakage freedom still holds once SMC is implemented as a concrete piece of software? As a step toward solving this problem, we use the proof assistant Rocq to formalize the security claims of an SMC stack. We develop a method based on an interpreter for a subset of the π -calculus in which protocols can be modeled as programs and then input traces verified for correctness and information leakage freedom. Thanks to this approach, the properties of SMC can be established in a clearly defined trusted base that can be reused to verify other SMC stacks.
Noninterference theory aims at ensuring the absence of covert channels among different security levels. As far as the verification of information-flow properties via equivalence checking is concerned, in nondeterministic and probabilistic settings weak bisimilarity has turned out to be adequate only for standard systems, while branching bisimilarity has proven to be appropriate for reversible systems too. In this paper we investigate noninterference for stochastically timed systems represented in the interactive Markov chain model of Hermanns. After recasting a selection of noninterference properties via Markovian variants of weak and branching bisimilarities, we study their preservation and compositionality aspects, build their taxonomy, and compare it with the nondeterministic and probabilistic taxonomies. We show the adequacy of our proposal through some examples about a database management system.
Testing connected cyber-physical systems (CPS) is a complex task. Connected CPS feature complex stochastic dynamic behaviour in interaction with the physical and human environment as well as communication over networks. Devising an oracle for testing connected CPS is a challenge; the oracle should be able to quantitatively reason about the stochastic nature of the interactions between the CPS and its environment. The quantitative reasoning should be sensitive to significant deviations in the dynamics and neglect minor deviations, e.g., due to measurement errors. To address this challenge, we provide the mathematical framework for conformance testing of connected CPS. We define a quantitative measure of closeness for two distributions of trajectories (i.e., output distributions from two distinct stochastic systems that are provided with the same input stimuli) that allows for capturing significant temporal and spatial deviations and neglecting subtle ones. This measure forms the basis for our notion of stochastic conformance, which determines when two stochastic systems conform to each other. We implement our proposed notion of stochastic conformance and compare our notion against a state-of-the-art baseline by applying both approaches to a case study involving a platoon of connected vehicles. Our notion detects a variety of different types of faults whilst allowing subtle deviations resulting from naturally occurring perturbations inherent to CPS.
We provide a constructive proof for the convergence of Dolev et al. BFS spanning tree algorithm running under the general assumption of an unfair daemon. Already known proofs of this algorithm are either using non-constructive principles (e.g., proofs by contradiction) or are restricted to less general execution daemons (e.g., weakly fair). In this work, we address these limitations by defining the well-founded orders and potential functions ensuring convergence in the general case. The proof has been fully formalized in PADEC, a Coq/Rocq-based framework for certification of self-stabilization algorithms.
Building systems that do not violate confidentiality of data through accidental information leakage is an increasingly important challenge. This is especially true for security-critical systems that handle sensitive information. A well-known obstacle for building secure systems is that security properties, such as confidentiality, are only addressed in late development phases. To combat this, information flow control by-construction (IFbC) was proposed. Similarly to correctness-byconstruction for functional correctness, it aims at building systems such that they have a secure information flow by-construction. This paper presents an extension of that work in which we scale IFbC to the software architectural level for component-based systems. Our approach allows software architects to create a high-level design of the system using UML component models with explicit provided and required interfaces. We provide information flow specifications for the interfaces of components, which integrates the security concerns of the system in the design phase. We then demonstrate how the individual components can be realized according to information flow control by-construction, such that they adhere to their interface specifications. We provide rules for compatibility of interfaces and implementations that ensure confidential information flow, and prove that all component-based systems that can be constructed by our approach satisfy their security properties. In this way, we allow flexible architectural modeling of component-based systems combined with strong confidentiality guarantees from information flow control by-construction. Finally, we present the tool ArchFlow which assists developers with creating secure component-based systems.
IoT and smart systems frequently rely on publish-subscribe (pub/sub) middlewares like MQTT or DDS. However, current coordination solutions often lack formal rigour, posing risks in mission-critical applications, or suffer from excessive complexity, hindering practical deployment and increasing the likelihood of errors. This paper addresses these challenges by integrating AbU, a recently introduced formal model based on Event-Condition-Action (ECA) rules and attribute-based communication, with standard pub/sub middlewares. We present a synchronization protocol that leverages pub/sub primitives to implement AbU's transactional communication semantics. We prove the correctness of this protocol, demonstrating that it accurately reflects the underlying system dynamics. This integration of a formal ECA-based programming model with pub/sub offers a compelling balance between rigorous guarantees and practical applicability for coordinating IoT and smart systems.
With the increasing autonomous capabilities of distributed cyber-physical systems, the complexity of their models also increases significantly, thus continually posing challenges to existing formal methods for safety verification. In contrast to model checking, monitoring emerges as an effective lightweight, yet practical verification technique capable of delivering results of practical importance with better scalability. Monitoring involves analyzing logs from an actual system to determine whether a specification (such as a safety property) is violated. Monitoring techniques, such as those using reachability methods, may fail to produce results when dealing with complex models like Deep Neural Networks (DNNs). We propose here a novel statistical approach for monitoring that is able to generate results with high probabilistic guarantees. We evaluate our monitoring technique on three case studies.
This tutorial concerns the use of a novel model of coordination of distributed systems. The model combines ideas from choreographic approaches and smart contracts. More precisely, application protocols regulating the coordination of a distributed application are rendered as global views that specify the expected behaviour of the system. Unlike in standard choreographic models though, participants are not necessarily obtained by projection from global views and can behave in completely unexpected ways. The adopted countermeasure to erroneous or malicious behaviour of participants is the one adopted in smart contracts: disabled interactions are just ignored.
Current choreography-based approaches to the specification and implementation of distributed systems lack support when it comes to program understanding. In particular, we miss systematic methodologies and algorithms to take a message-passing program written in a mainstream programming language and automatically produce a global description of all its communication behaviors. This helps understanding the program interaction patterns and also highlights possible unexpected behaviors to support debugging. We discuss the requirements and difficulties of the approach we envisage. Through concrete examples we outline the kind of global descriptions we want to obtain.
The Real-Driving Emissions (RDE) is a regulation set by the European Union Commission. Its main purpose is to set out the foundations for vehicle emission tests. In this paper, we present LolaPrompts, which exploits runtime monitoring to assist the drivers in performing driving scenarios that confirm to the RDE constraints. It provides the drivers with audible prompts and explanations in order to produce a valid RDE test. The purpose of our tool, LolaPrompts, is to make RDE test available for the general public and allow them to scrutinise the emission profile of their vehicles.
Symmetric nets (SN), including their stochastic extension (SSN), are a type of high-level Petri net (HLPN) known for their structured syntax, which aids in efficient analysis. Their dynamics is described by a quotient state-transition system (SRG) linked to a lumped Markov chain. State-space analysis and stochastic model checking are supported by tools like GreatSPN [4, 7] and COSMOS [3, 9], then a toolset has become available for structural analysis of SN: SNexpression [2,10]. This framework is based on algebraic calculi to derive properties in a symbolic manner. The paper presents a novel component for operating at the net level by manipulating matrices of structural expressions directly. This approach enables a coherent definition of stochastic parameters in SSNs with several transition priority levels and extends the analysis capabilities by identifying independent classes of transition instances. The paper illustrates the new SNexpression functionalities of matrix structural calculi on two examples.
Assessing the correctness of distributed and parallel applications is notoriously difficult due to the complexity of the concurrent behaviors and the difficulty to reproduce bugs. In this context, Dynamic Partial Order Reduction (DPOR) techniques have proved successful in exploiting concurrency to verify applications without exploring all their behaviors. However, they may lack of efficiency when tracking non-systematic bugs of real size applications. In this paper, we suggest two adaptations of the Optimal Dynamic Partial Order Reduction (ODPOR) algorithm with a particular focus on bug finding and explanation. The first adaptation is an out-of-order version called RFS ODPOR which avoids being stuck in uninteresting large parts of the state space. Once a bug is found, the second adaptation takes advantage of ODPOR principles to efficiently find the origins of the bug.
We present an empirical evaluation of Large Language Models (LLMs) in understanding semantic-preserving code transformations such as copy propagation and constant folding. Our results show that LLMs fail to recognize semantic equivalence in approximately 41
Biernacka et al. recently proposed zipper semantics, a semantics format from which sound and complete abstract machines for non-deterministic languages can be automatically derived.We present a new style of zipper semantics, called leaf-first, in which we express the semantics of two extensions of HOπ, a higher-order version of the π-calculus: one with passivation and the other with join patterns.The leaf-first style is better suited than the original one to express phenomena occurring in process calculi semantics such as scope extrusion, which is observable with passivation and complex with join patterns.
AuDaLa is a recently introduced programming language that follows the new data autonomous paradigm. In this paradigm, small pieces of data execute functions autonomously. Considering the paradigm and the design choices of AuDaLa, it is interesting to determine the expressiveness of the language and to create verification methods for it. In this paper, we take our first steps to such a verification method by implementing Turing machines in AuDaLa and proving that implementation correct. This also proves that AuDaLa is Turing complete.
We generalize the DeGroot model for opinion dynamics to better capture realistic social scenarios. We introduce a model where each agent has their own individual cognitive biases . Society is represented as a directed graph whose edges indicate how much agents influence one another. Biases are represented as the functions in the square region [ - 1 , 1 ] 2 and categorized into four sub-regions based on the potential reactions they may elicit in an agent during instances of opinion disagreement . Under the assumption that each bias of every agent is a continuous function within the region of receptive but resistant reactions ( R ), we show that the society converges to a consensus if the graph is strongly connected. Under the same assumption, we also establish that the entire society converges to a unanimous opinion if and only if the source components of the graph-namely, strongly connected components with no external influence-converge to that opinion. We illustrate that convergence is not guaranteed for strongly connected graphs when biases are either discontinuous functions in R or not included in R . We showcase our model through a series of examples and simulations, offering insights into how opinions form in social networks under cognitive biases.
We address the problem of synthesizing a timed automaton from a set of optimised timed scenarios, and present a simple, efficient algorithm that solves the problem. Under a simplifying assumption about the set of scenarios we show that our synthesized automaton has the minimal number of clocks in the entire class of language-equivalent automata.
Formal verification of distributed protocols is challenging and usually requires great human effort. Ivy, a state-of-the-art formal verification tool for modeling and verifying distributed protocols, automates this tedious process by leveraging a decidable fragment of first-order logic. Observing the successful adoption of Ivy for verifying consensus protocols, we examine its practicality in verifying rollback-prevention protocols for Trusted Execution Environments (TEEs). TEEs suffer from rollback attacks, which can revert confidential applications’ states to stale ones to compromise security. Recently, designing distributed protocols to prevent rollback attacks has attracted significant attention. However, the lack of formal verification of these protocols leaves them potentially vulnerable to security breaches. In this paper, we leverage Ivy to formally verify a rollback-prevention protocol, namely the TIKS protocol in ENGRAFT (Wang et al. , CCS 2022). We select TIKS because it is similar to other rollback-prevention protocols and is self-contained. We detail the verification process of using Ivy to prove a rollback-prevention protocol, present lessons learned from this exploration, and release the proof code to facilitate future research ( https://github.com/wwl020/TIKS-Proof-in-Ivy ). To the best of our knowledge, this is the first endeavor to explain the formal verification of a rollback-prevention protocol in detail.
