We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM changed only what the developer authorised. We present CAPRI, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract. Prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes are retained for audit. We evaluate five workflows on twelve failed proofs from four developments, with three replicates per task and condition, giving 180 runs and 138 valid repairs. Of 144 terminal candidates accepted by Isabelle, six had modified protected text; all arose in iterative workflows that could edit a complete theory. A proof-body-only interface produced 29/36 valid repairs and no contract violations, compared with 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36; these figures compare complete workflows rather than individual mechanisms. A separate post hoc OpenRouter campaign found no improvement in the designated Luna comparisons. A Sol configuration with matched demonstrations produced 33/36 repairs, compared with 29/36 in the frozen OpenAI Responses condition, but the difference was not statistically significant in a one-sided exact McNemar test (p=0.0625).

Testing concurrent systems is challenging due to their complex interactions and behaviours, along with the difficulty in reproducing failures. We propose a sound strategy for testing concurrent mobile applications by extracting use cases that capture interleavings of behaviours of existing test cases for individual features. These use cases are then used to create a formal model that is the input for a refinement checking approach to generate test cases that are still sequential but exercise the execution of concurrent features. We introduce a conformance relation, cspioq, which considers quiescent behaviour (absence of output). This relation is based on cspio (which is itself inspired by ioco); cspio does not take quiescence behaviour into account. While ioco as well as cspioco (a denotational semantics for ioco based on CSP) rely on suspension traces, our approach adopts the traces model annotated with a special event to represent quiescence. This allowed us to reuse our previous theory and test case generation strategy for sequential systems in a conservative way. We also analyse the complexity of automatically generating test cases. For implementation efficiency, we optimise the strategy by directly interleaving steps of existing test cases and show that this preserves soundness. Moreover, we provide tool support for every phase of the approach. Finally, we present the results of an empirical evaluation designed to measure the effectiveness of the overall strategy in terms of test coverage and bug detection. The results indicate that our approach yields higher coverage and higher bug detection rates compared to the set of tests originally developed by our industrial partner (Motorola) engineers.

UML is widely adopted for modelling object-oriented software systems, including diagrams that cover the several facets of the entire development life cycle. Approaches to formal semantics of UML tend to concentrate on individual diagrams and, so far, no complete, standard, semantics is available. Here, we explore a different path and define a natural-language semantics for UML models that embody state machines and composite structure diagrams. We then integrate with the NAT2TEST strategy to provide means for an integrated framework for the validation (via simulation) and verification (via testing - QuickChick, interactive theorem proving - Rocq, and model checking - FDR) of UML models. The integration is based on a systematic process (mapping rules), and its soundness has been validated considering an independent reference formal semantics. The developed tool support uses ATL to implement the translation from UML models to natural-language requirements directly based on the proposed mapping rules. We illustrate our contributions and tool support with respect to two case studies: the classical Dijkstra's dining philosophers problem, and a distributed ring-buffer model.

Large language models can propose proofs for interactive theorem provers, but a successful build does not show the surrounding verification task was preserved. We study this problem in an Isabelle development of a sampled-data double-tank controller. The work began with nine theories and ten unfinished obligations, grew to a 16-theory build without sorry, oops, added axiomatisation, or oracle use, and accumulated 23 stable and 36 broken proof states. A retrospective audit found material changes in 16 of the 100 original declarations, including a weakened end-to-end assurance theorem that assumed three of the four requirements in its conclusion. We used CAPRI, a contract-aware proof-repair tool, to govern a reconstruction by combining Isabelle acceptance with an independent check of repository changes against machine-readable edit contracts. The reconstruction discharged all ten scoped obligations within the original nine-theory structure. A secondary replay by a co-author reproduced the R10 build, contract checks, control tests, and principal audit findings; independent replication remains future work. Operational end-to-end verification remains incomplete: we still need to connect operational executions to the reconstructed quantitative trace contract, a task requiring an extended contract.

In an industrial context, ad-hoc/manual testing strategies, using natural language, still seem to be highly prevalent since natural language descriptions are, more likely, easier to understand. Still, the lack of rigor can generate inaccurate tests. Aligned with other modern approaches, we promote the use of natural language descriptions with rigorously defined underlying semantics. As a distinguished feature of our approach, we cover the entire (direct engineering) testing process, from requirements to manual or automated test cases generated automatically. Requirements written in a controlled natural language are parsed, and their semantics are automatically modeled using the CSP process algebra. To address soundness and deal with different abstraction levels, we formalize the concept of a domain model, in which additional information, such as hierarchical composition and a dependence relation among test steps, is defined. Then, sound test cases are generated from the inferred scenarios using the cspio conformance relation. These test cases, still expressed in CSP, can then be linearized back to natural language to allow manual execution or directly translated into test scripts for automated execution.

The Ethereum blockchain has a gas system that associates operations with a cost in gas units. Two central concepts of this system are the gas limit assigned by the issuer of a transaction and the gas used by a transaction. The former is a budget that must not be exhausted before the completion of the transaction execution; otherwise, the execution fails. Therefore, it seems rather essential to determine the minimum gas limit that ensures the execution of a transaction will not abort due to the lack of gas. Despite its practical relevance, this concept has not been properly addressed. In the literature, gas used and minimum gas limit are conflated. This paper proposes a precise notion of minimum gas limit and how it can differ from gas used by a transaction; this is also demonstrated with a quantitative study on real transactions of the Ethereum blockchain. Another significant contribution is the proposition of a fairly precise estimator for each of the two metrics. Again, the confusion between these concepts has led to the creation of estimators only for the gas used by a transaction. We demonstrate that the minimum gas limit for the state of the Ethereum blockchain (after the block) B can serve as a near-perfect estimation for the execution of the transaction at block B + Δ , where Δ≤ 11 ; the same holds for estimating gas used. These precise estimators can be very valuable in helping the users predict the gas budget of transactions and developers in optimising their smart contracts; over and underestimating gas used and minimum gas limit can lead to a number of practical issues. Overall, this paper serves as an important reference for blockchain developers and users as to how the gas system really works.

We present a formal theory for analysing causality in cyber-physical systems. To this end, we extend the theory of actual causality by Halpern and Pearl to cope with the continuous nature of cyber-physical systems. Based on our theory, we develop an analysis technique that is used to uncover the causes for examples of failures resulting from verification, which are represented as continuous trajectories. We develop a search-based technique to efficiently produce such causes and provide an implementation for such a technique. Moreover, we apply our solution to case studies (a suspension system and a connected platoon) and benchmark systems to evaluate its effectiveness; in the experiment, we show that we were able to detect causes for inserted faults.

Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

The lack of systematic and, particularly, mechanised support to ensure a safe creation and upgrade of smart contracts has led to the deployment of instances with flaws that have been thoroughly exploited, putting digital assets at risk. Formal verification can potentially help to eliminate these high impact flaws, particularly by allowing one to check whether smart contracts obey some desired properties. We have already proposed the concept of a trusted deployer to address these issues. In this work we present the detailed design of a public, open-source, and off-chain tool that supports the creation and upgrade of smart contracts, ensuring that they meet corresponding formal specifications. We detail the tool's overall architecture, its usage, and its applicability to real-world smart contracts.

In our previous work, we proposed a verification framework that shifts from the “code is law” to a new “specification is law” paradigm related to the safe evolution of smart contracts. The framework proposed there relaxed the well-established requirement that, once a smart contract is deployed in a blockchain, its code is expected to be immutable. More flexibly, contracts are allowed to be created and upgraded provided they meet a corresponding formal specification that was fixed. In the current paper, we extend this framework to allow specifications to evolve, provided a refinement notion is preserved. We propose a notion of specification refinement tailored for smart contracts and a methodology for checking it. In addition to weakening preconditions and strengthening postconditions and invariants, we allow for the change of data representation and interface extension. Thus, we are able to reason about a significantly wider class of smart contract evolution histories, when contrasted with the original framework. The new framework is centred around a trusted deployer : an off-chain service that formally verifies and enforces the notions of implementation conformance and specification refinement. We have investigated its applicability to the safe deployment and upgrade of contracts implementing widely used Ethereum standards (the ERC20 Token Standard, the ERC3156 Flash Loans, the ERC1155 Multi Token Standard and The ERC721 standard for Non-Fungible Tokens); we handle evolutions possibly involving changes in data representation and interface extensions.

UML is widely adopted for modelling object-oriented software systems, including diagrams that cover the several facets of the entire development life cycle. Approaches to formal semantics of UML tend to concentrate on individual diagrams and, so far, no complete, standard, semantics is available. Here, we explore a different path and define a natural-language semantics for a component UML model that embodies state machines and composite structure diagrams. We then integrate with the NAT2TEST strategy to provide means for analysis (via model checking and theorem proving), simulation and testing. The integration is based on a systematic process (mapping rules), and its soundness has been validated considering an independent reference formal semantics. The developed tool support automates the translation from UML models to natural-language requirements directly based on the proposed mapping rules. We illustrate our contributions and tool support with respect to two case studies: the classical Dijkstra's dining philosophers problem, and a distributed ring-buffer model.

Compositional deadlock analysis of process networks is a well-known challenge. We propose a compositional deadlock analysis strategy for timed process networks, more specifically, those obtained from Simulink multi-rate block diagrams. We handle models with both acyclic and cyclic communication graphs. Particularly, the latter naturally happens in Simulink models with feedback, among other kinds of cycles. Since there is no general solution to analyse cyclic models in a compositional way, we explore the use of behavioural patterns that allow the verification to be carried out in a compositional fashion. We represent process networks in tock-CSP, a dialect of CSP that allows modelling time aspects using a special tock event. The verification approach is implemented as a new package in CSP-Prover, a theorem prover for CSP which is itself implemented in Isabelle/HOL. To illustrate the overall approach and, particularly, how it can scale, we consider several variations of an actuation system with increasing complexity. We show that the examples are instances of the client/server and the asynchronous dynamic timed behaviour patterns. These patterns and all verification steps are formalised using CSP-Prover.

Developers tend to be reluctant to provide formal specifications for software components; even well-established design-by-contract (DbC) properties like invariants, pre- and postconditions are neglected. This has hindered a more widely practical dissemination of the DbC paradigm. In this paper, we employ state-of-the-art NL processing technologies, using Large Language Models (LLMs), particularly, ChatGPT, to automatically infer formal specifications from component textual behavioural descriptions. More specifically, we implemented a framework (DbC-GPT), parameterised by a context, which is able to generate postcondition specifications for smart contract functions implemented in Solidity. The output of DbC-GPT is in the notation of the solc-verify tool (a verifier for Solidity) that is used to: (i) check the syntax of the inferred specification; and (ii) verify whether a reference implementation conforms to this specification. This is carried out in a loop in such a way that the DbC-GPT context is iteratively improved with verification counterexamples. To evaluate DbC-GPT, we have used some Ethereum standards (ERC20, ERC721, and ERC1155) and compared the precision of the generated specifications for several GPT contexts that consider information of these standards in isolation as well as their combination.

In previous work, we have proposed an efficient technique, using local analysis, to ensure livelock freedom of CSP systems modelled in the context of a component model, BRIC, with asynchronous compositions. Applicability of this analysis, however, imposed strong restrictions on the CSP models. In this paper, we propose a significantly more elaborate technique for establishing livelock freedom of BRIC components. We present new definitions for our local conditions to deal with asynchronous models, as well as parametrised recursive processes, and establish the soundness of this new approach. Finally, we use an implementation of our technique to demonstrate its effectiveness. We compare the performance of our approach with that of two other techniques for livelock-freedom verification, namely, FDR4 and SLAP, and demonstrate that our approach affords significant gains.

Transaction costs are a barrier to the wide adoption of decentralized applications. To address this issue, this paper proposes a framework to optimize transaction fees by carrying out a conflict-avoiding packaging of multiple smart-contract calls into a single transaction. It relies on two main concepts: a way to optimize the bundling of transactions with a conflict-avoiding packaging strategy and a way to execute such bundles with a package-processing methodology. We illustrate our framework and the gas economy it can bring with a case study where we analyze a popular Ethereum smart contract.

It is well-recognised that testing concurrent systems poses challenges due to their complex interactions and behaviours, as well as the difficulty to reproduce failures. We propose a sound strategy for testing concurrent mobile applications by first extracting use cases that capture interleavings of behaviours of existing test cases for individual features. From these use cases, we generate test cases that are still sequential but exercise the execution of concurrent features. Our approach incorporates a dependency analysis to ensure a consistent execution order of test steps, avoiding incoherent sequences, like sending a message without establishing an internet connection. We introduce a conformance relation, 𝐜𝐬𝐩𝐢𝐨_𝐪 , based on cspio , but extended to consider quiescent behaviour (output absence) as in ioco , a widely recognised conformance relation for formal software testing. We then optimise the strategy, which involves permuting test steps without the need to generate use cases but preserving soundness. We discuss tool support and conduct an empirical evaluation to assess the effectiveness of the overall strategy in terms of test coverage and bug detection. The results indicate that our approach yields higher coverage and potential bug detection compared to the set of tests generated by Motorola engineers.

Model-based engineering emerged as an approach to tackle the complexity of current system development. In particular, compositional strategies assume that systems can be built from reusable and loosely coupled units. However, it is still a challenge to ensure that desired properties hold for component integration. We present a component-based model for UML, including a metamodel, well-formedness conditions and formal semantics via translation into BRIC; the presentation of the semantics is given by a set of rules that cover all the metamodel elements and map them to their respective BRIC denotations. We use our previous work on BRIC as an underlying (and totally hidden) component development framework so that our approach benefits from all the formal infrastructure developed for BRIC using CSP. Component composition, specified via UML structural diagrams, ensures adherence to classical concurrent properties: our focus is on the preservation of deadlock freedom. Automated support is developed as a plug-in to the Astah modelling tool. Verification is carried out using FDR (a model checker for CSP); we address scalability using compositional reasoning (inherent to the approach) and behavioural patterns. The formal reasoning is transparent to the user: a distinguishing feature of our approach is its support for traceability. For instance, when FDR uncovers a deadlock, a sequence diagram is constructed from the deadlock trace and presented to the user at the modelling level. The overall approach is illustrated with a running example and two additional case studies.

We dedicate this paper with great respect and friendship to He Jifeng on the occasion of his 80th birthday. Our research group owes much to him. The authors have over 150 publications on unifying theories of programming (UTP), a research topic Jifeng created with Tony Hoare. Our objective is to recount the history of Circus (a combination of Z, CSP, Dijkstra’s guarded command language, and Morgan’s refinement calculus) and the development of Isabelle/UTP. Our paper is in two parts. (1) We first discuss the activities needed to model systems: we need to formalise data models and their behaviours. We survey our work on these two aspects in the context of Circus. (2) Secondly, we describe our practical implementation of UTP in Isabelle/HOL. Mechanising UTP theories is the basis of novel verification tools. We also discuss ongoing and future work related to (1) and (2). Many colleagues have contributed to these works, and we acknowledge their support.

State machines are widely used in industry and academia to capture behavioural models of control. They are included in popular notations, such as UML and its variants, and used (sometimes informally) to describe computational artefacts. In this paper, we present laws for state machines that we prove sound with respect to a process algebraic semantics for refinement, and complete, in that they are sufficient to reduce an arbitrary model to a normal form that isolates basic (action and control) elements. We consider two variants of UML-like state machines, both enriched with facilities to deal with time budgets, timeouts and deadlines over triggers and actions. In the first variant, machines are self-contained components, declaring all the variables, events and operations that they require or define. In contrast, in the second variant, machines are open, like in UML for instance. Laws for open state machines do not depend on a specific context of variables, events and operations, and normalization uses a novel operator for open-machine (de)composition. Our laws can be used in behaviour-preservation transformation techniques. Their applications are automated by a model-transformation engine.

This paper proposes the adoption of modern Software Engineering techniques in the context of the development of robotic systems. Particularly, we use a design language, RoboChart, and a tool set, RoboTool, which support modelling, verification (via model checking) and simulation of such systems, among other facilities. Our application domain is an Unmanned Aerial Vehicle (UAV) and its control system, targetting at competition challenges. This system needs to be capable to perform navigation tasks in indoor environments and achieve some goals like detecting and finding objects, landing spots and maintaining a stable flight. We emphasise the important role of a design model both concerning formal verification of classical and domain-specific properties and as a basis for a systematic strategy to develop trustworthy implementations