1 citations · 1 across the 9 of their papers we have counts for
9 papers
Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study
Jim Woodcock, Gabriel Leite, Augusto Sampaio +1
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 proble…
CAPRI: Contract-Aware Proof Repair for Isabelle
Jim Woodcock, Gabriel Leite, Augusto Sampaio +1
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 change…
Engineering Reliable Autonomous Systems: Challenges and Solutions
Marie Farrell, Matt Luckcuck, Angelo Ferrando +28
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…
Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
Ran Wei, Le Zhu, Haochi Wang +4
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-…
Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
Dustin Bryant, Jim Woodcock, Simon Foster
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 th…
Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version)
Kangfeng Ye, Roberto Metere, Jim Woodcock +1
Formal verification is crucial for ensuring the robustness of security protocols against adversarial attacks. The Needham-Schroeder protocol, a foundational authentication mechanis…
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
Simon Foster, Chung-Kil Hur, Jim Woodcock
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…
RoboCertProb: Property Specification for Probabilistic RoboChart Models
Kangfeng Ye, Jim Woodcock
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…
Checking and Automating Confidentiality Theory in Isabelle/UTP
Lex Bailey, Jim Woodcock, Simon Foster +1
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 sy…