arXiv subjects

Jim Woodcock

Publications and source records attributed to Jim Woodcock.

At least 19 recordsLinked to original sources

arXiv2026

Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study

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.

cs.SE↗

arXiv2026

A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects

In this paper, we systematically investigate the connection between linearizable objects and forward simulation. We prove that the sets of linearizable objects satisfying wait-freedom (resp., lock-freedom or obstruction-freedom) form a bounded join-semilattice under the forward simulation relation, and that the sets of linearizable objects without liveness constraints form a bounded lattice under the same relation. Thus, forward simulation is not only a proof technique for linearizability but also induces an algebraic hierarchy of linearizable objects. As part of our lattice result, we propose an equivalent characterization of linearizability by reducing checking linearizability w.r.t. sequential specification $Spec$ into checking forward simulation w.r.t. an object $\mathcal{U}_{Spec}$.

cs.DC↗

arXiv2026

CAPRI: Contract-Aware Proof Repair for Isabelle

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$).

cs.SE↗

arXiv2026

Engineering Reliable Autonomous Systems: Challenges and Solutions

Engineering reliable autonomous systems is an important and growing topic in computer science. As autonomous systems become more prevalent, easy-to-use techniques for building them reliably are increasingly important. This workshop report captures and expands on the discussions at the Lorentz Center Workshop "Engineering Reliable Autonomous Systems" (ERAS), held from 10 to 14 June 2024. The workshop was co-organised by the organisers of the Workshop on Formal Methods for Autonomous Systems (FMAS) and the Workshop on Agents and Robots for reliable Engineered Autonomy (AREA). It brought together members of the FMAS and AREA communities, industry practitioners, and representatives from sectors where autonomous systems pose distinctive engineering challenges. The workshop focused on three main research topics: techniques for verification and validation of autonomous systems; engineering real-world autonomous systems; and software architectures for safe autonomous systems. Its main outcome is a catalogue of challenges in these areas and, most importantly, a pathway to solutions. Some challenges can already be tackled by techniques that are well known in academia but have not yet become regularly used in practice. Other challenges remain unresolved and require further research. This roadmap is intended to support future research and industrial collaboration.

cs.RO↗

arXiv2026

Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering

Vibe coding -- accepting LLM-generated source from natural-language intent with minimal review -- is fast and may be adequate for low-criticality consumer software. But for safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification: large language models (LLMs) provide no formal correctness guarantees, and existing remedies target verification-aware languages (Dafny, Verus, Lean) that are scarce in pretraining data and absent from industrial toolchains. This paper closes the gap. We present Forge (Formal method Oriented Refinement loop for GEnerated code): a closed-loop pipeline that guides vibe coding through formal verification using established Model-Driven Engineering (MDE) infrastructure. Through vibe coding, we generate Java source code; our pipeline then extracts -- via model transformations -- formal artefacts in three different formalisms, each checked by a complementary verifier: deductive verification (Dafny), Communicating Sequential Processes (CSP) refinement via the Failures-Divergences Refinement checker (FDR4), and theorem proving using Z-Machines in Isabelle; every verification failure becomes a structured correction prompt that drives the next code-generation iteration. The LLM is the draft generator, the MDE chain is the discriminator, and the developer never has to read the formal models. Empirically, we find that the pipeline produces standards-relevant verification evidence for LLM-generated Java -- a step toward certification.

cs.SE↗

arXiv2026

Software Engineering for Self-Adaptive Robotics: A Research Agenda

Self-adaptive robotic systems operate autonomously in dynamic and uncertain environments, requiring robust real-time monitoring and adaptive behaviour. Unlike traditional robotic software with predefined logic, self-adaptive robots exploit artificial intelligence (AI), machine learning, and model-driven engineering to adapt continuously to changing conditions, thereby ensuring reliability, safety, and optimal performance. This paper presents a research agenda for software engineering in self-adaptive robotics, structured along two dimensions. The first concerns the software engineering lifecycle, requirements, design, development, testing, and operations, tailored to the challenges of self-adaptive robotics. The second focuses on enabling technologies such as digital twins and AI-driven adaptation, which support runtime monitoring, fault detection, and automated decision-making. We identify open challenges, including verifying adaptive behaviours under uncertainty, balancing trade-offs between adaptability, performance, and safety, and integrating self-adaptation frameworks like MAPE K/MAPLE-K. By consolidating these challenges into a roadmap toward 2030, this work contributes to the foundations of trustworthy and efficient self-adaptive robotic systems capable of meeting the complexities of real-world deployment.

cs.SE↗

arXiv2025

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem

This paper presents a formalized analysis of the sigmoid function and a fully mechanized proof of the Universal Approximation Theorem (UAT) in Isabelle/HOL, a higher-order logic theorem prover. The sigmoid function plays a fundamental role in neural networks; yet, its formal properties, such as differentiability, higher-order derivatives, and limit behavior, have not previously been comprehensively mechanized in a proof assistant. We present a rigorous formalization of the sigmoid function, proving its monotonicity, smoothness, and higher-order derivatives. We provide a constructive proof of the UAT, demonstrating that neural networks with sigmoidal activation functions can approximate any continuous function on a compact interval. Our work identifies and addresses gaps in Isabelle/HOL's formal proof libraries and introduces simpler methods for reasoning about the limits of real functions. By exploiting theorem proving for AI verification, our work enhances trust in neural networks and contributes to the broader goal of verified and trustworthy machine learning.

cs.LO↗

arXiv2025

Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version)

Formal verification is crucial for ensuring the robustness of security protocols against adversarial attacks. The Needham-Schroeder protocol, a foundational authentication mechanism, has been extensively studied, including its integration with Physical Layer Security (PLS) techniques such as watermarking and jamming. Recent research has used ProVerif to verify these mechanisms in terms of secrecy. However, the ProVerif-based approach limits the ability to improve understanding of security beyond verification results. To overcome these limitations, we re-model the same protocol using an Isabelle formalism that generates sound animation, enabling interactive and automated formal verification of security protocols. Our modelling and verification framework is generic and highly configurable, supporting both cryptography and PLS. For the same protocol, we have conducted a comprehensive analysis (secrecy and authenticity in four different eavesdropper locations under both passive and active attacks) using our new web interface. Our findings not only successfully reproduce and reinforce previous results on secrecy but also reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios, even in cases where secrecy is compromised. We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming, and our analysis shows that it is secure for deriving a session key with required authentication. These highlight the advantages of our novel approach, demonstrating its robustness in formally verifying security properties beyond conventional methods.

cs.CR↗

arXiv2025

Probabilistic modelling and safety assurance of an agriculture robot providing light-treatment

Continued adoption of agricultural robots postulates the farmer's trust in the reliability, robustness and safety of the new technology. This motivates our work on safety assurance of agricultural robots, particularly their ability to detect, track and avoid obstacles and humans. This paper considers a probabilistic modelling and risk analysis framework for use in the early development phases. Starting off with hazard identification and a risk assessment matrix, the behaviour of the mobile robot platform, sensor and perception system, and any humans present are captured using three state machines. An auto-generated probabilistic model is then solved and analysed using the probabilistic model checker PRISM. The result provides unique insight into fundamental development and engineering aspects by quantifying the effect of the risk mitigation actions and risk reduction associated with distinct design concepts. These include implications of adopting a higher performance and more expensive Object Detection System or opting for a more elaborate warning system to increase human awareness. Although this paper mainly focuses on the initial concept-development phase, the proposed safety assurance framework can also be used during implementation, and subsequent deployment and operation phases.

cs.RO↗

arXiv2024

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL

Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct formal proofs demonstrating satisfaction of certain critical properties in support of high-assurance software engineering. To ensure coherent results between execution and proof, we need unifying semantics and automation. In this paper, we mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework. ITrees are coinductive structures that allow us to encode infinite labelled transition systems, yet they are inherently executable. We use ITrees to create verification tools for stateful imperative programs, concurrent programs with message passing in the form of the CSP and \Circus languages, and abstract system models in the style of the Z and B methods. We demonstrate how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model. Finally, we demonstrate how ITrees can be executed using the Isabelle code generator to support the animation of models.

cs.LO↗

arXiv2024

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving

Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic programs are ubiquitous, including having a significant impact on machine intelligence. While many probabilistic algorithms have been used in practice in different domains, their automated verification based on formal semantics is still a relatively new research area. In the last two decades, it has attracted much interest. Many challenges, however, remain. The work presented in this paper, probabilistic unifying relations (ProbURel), takes a step towards our vision to tackle these challenges. Our work is based on Hehner's predicative probabilistic programming, but there are several obstacles to the broader adoption of his work. Our contributions here include (1) the formalisation of its syntax and semantics by introducing an Iverson bracket notation to separate relations from arithmetic; (2) the formalisation of relations using Unifying Theories of Programming (UTP) and probabilities outside the brackets using summation over the topological space of the real numbers; (3) the constructive semantics for probabilistic loops using Kleene's fixed-point theorem; (4) the enrichment of its semantics from distributions to subdistributions and superdistributions to deal with the constructive semantics; (5) the unique fixed-point theorem to simplify the reasoning about probabilistic loops; and (6) the mechanisation of our theory in Isabelle/UTP, an implementation of UTP in Isabelle/HOL, for automated reasoning using theorem proving. We demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination of probabilistic loops.

cs.LO↗

arXiv2024

RoboCertProb: Property Specification for Probabilistic RoboChart Models

RoboChart is a core notation in the RoboStar framework which brings modern modelling and formal verification technologies into software engineering for robotics. It is a timed and probabilistic domain-specific language for robotics and provides a UML-like architectural and state machine modelling. This work presents RoboCertProb for specifying quantitative properties of probabilistic robotic systems modelled in RoboChart. RoboCertProb's semantics is based on PCTL*. To interpret RoboCertProb over RoboChart models, we give a Markov semantics (DTMCs and MDPs) to RoboChart, derived from its existing transformation semantics to the PRISM language. In addition to property specification, RoboCertProb also entitles us to configure loose constants and unspecified functions and operations in RoboChart models. It allows us to set up environmental inputs to verify reactive probabilistic systems not directly supported in probabilistic model checkers like PRISM because they employ a closed-world assumption. We implement RoboCertProb in an accompanying tool of RoboChart, RoboTool, for specifying properties and automatically generating PRISM properties from them to formally verify RoboChart models using PRISM. We have used it to analyse the behaviour of software controllers for two real robots: an industrial painting robot and an agricultural robot for treating plants with UV lights.

cs.LO↗

arXiv2024

State of the Art Report: Verified Computation

This report describes the state of the art in verifiable computation. The problem being solved is the following: The Verifiable Computation Problem (Verifiable Computing Problem) Suppose we have two computing agents. The first agent is the verifier, and the second agent is the prover. The verifier wants the prover to perform a computation. The verifier sends a description of the computation to the prover. Once the prover has completed the task, the prover returns the output to the verifier. The output will contain proof. The verifier can use this proof to check if the prover computed the output correctly. The check is not required to verify the algorithm used in the computation. Instead, it is a check that the prover computed the output using the computation specified by the verifier. The effort required for the check should be much less than that required to perform the computation. This state-of-the-art report surveys 128 papers from the literature comprising more than 4,000 pages. Other papers and books were surveyed but were omitted. The papers surveyed were overwhelmingly mathematical. We have summarised the major concepts that form the foundations for verifiable computation. The report contains two main sections. The first, larger section covers the theoretical foundations for probabilistically checkable and zero-knowledge proofs. The second section contains a description of the current practice in verifiable computation. Two further reports will cover (i) military applications of verifiable computation and (ii) a collection of technical demonstrators. The first of these is intended to be read by those who want to know what applications are enabled by the current state of the art in verifiable computation. The second is for those who want to see practical tools and conduct experiments themselves.

cs.CR↗

arXiv2023

Formally Verified Animation for RoboChart using Interaction Trees

RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based language for robotics. RoboChart supports shared variables and communication across entities in its component model. It has formal denotational semantics given in CSP. The semantic technique of Interaction Trees (ITrees) represents behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisation of ITrees, along with ITree-based CSP semantics and a Z mathematical toolkit in Isabelle/HOL, bring new applications of verification and animation for state-rich process languages, such as RoboChart. In this paper, we use ITrees to give RoboChart novel operational semantics, implement it in Isabelle, and use Isabelle's code generator to generate verified and executable animations. We illustrate our approach using an autonomous chemical detector model and a patrol robot model additionally exhibiting nondeterminism and using shared variables. With animation, we show two concrete scenarios for the chemical detector when the robot encounters different environmental inputs and three concrete scenarios for the patrol robot when its calibrated position is in different sections of a corridor. We also verify that the animated scenarios are truly trace refinements of the CSP denotational semantics of the RoboChart models using FDR, a refinement model checker for CSP. This ensures that our approach to resolving nondeterminism using CSP operators with priority is sound and correct.

cs.LO↗

arXiv2023

Checking and Automating Confidentiality Theory in Isabelle/UTP

The severity of recent vulnerabilities discovered on modern CPUs, e.g., Spectre [1], highlights how information leakage can have devas-tating effects to the security of computer systems. At the same time, it suggests that confidentiality should be promoted as a normal part of program verification, to discover and mitigate such vulnerabili-ties early in development. The theory we propose is primarily based on Bank's theory [2], a framework for reasoning about confidentiali-ty properties formalised in the Unifying Theories of Programming (UTP) [3]. We mechanised our encoding in the current implementa-tion of UTP in the Isabelle theorem prover, Isabelle/UTP [4]. We have identified some theoretical issues in Bank's original framework. Finally, we demonstrate how our mechanisation can be used to for-mally verify of some of the examples from Bank's work.

cs.CR↗

arXiv2023

A Manifesto for Applicable Formal Methods

Formal methods were frequently shown to be effective and, perhaps because of that, practitioners are interested in using them more often. Still, these methods are far less applied than expected, particularly, in critical domains where they are strongly recommended and where they have the greatest potential. Our hypothesis is that formal methods still seem not to be applicable enough or ready for their intended use. In critical software engineering, what do we mean when we speak of a formal method? And what does it mean for such a method to be applicable both from a scientific and practical viewpoint? Based on what the literature tells about the first question, with this manifesto, we lay out a set of principles that when followed by a formal method give rise to its mature applicability in a given scope. Rather than exercising criticism of past developments, this manifesto strives to foster an increased use of formal methods to the maximum benefit.

cs.SE↗

arXiv2022

A Pattern-based deadlock-freedom analysis strategy for concurrent systems

Local analysis has long been recognised as an effective tool to combat the state-space explosion problem. In this work, we propose a method that systematises the use of local analysis in the verification of deadlock freedom for concurrent and distributed systems. It combines a strategy for system decomposition with the verification of the decomposed subsystems via adherence to behavioural patterns. At the core of our work, we have a number of CSP refinement expressions that allows the user of our method to automatically verify all the behavioural restrictions that we impose. We also propose a prototype tool to support our method. Finally, we demonstrate the practical impact our method can have by analysing how it fares when applied to some examples.

cs.SE↗

arXiv2021

Proceedings First Workshop on Applicable Formal Methods

This volume contains the proceedings of the 1st International Workshop on Applicable Formal Methods (AppFM 2021), 23 November 2021, held online as part of the 24th International Symposium on Formal Methods (FM). The aim of the AppFM workshop is to bring together researchers who improve and evaluate existing formal approaches and new variants in practical contexts and support the transfer of these approaches to software engineering practice.

cs.SE↗