6 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…
Symmetry-Breaking De Novo Crystal Generation via Markovian Jump Diffusion
Van Khoa Nguyen, Alexandros Kalousis
Generating crystals has recently attracted significant interest due to their broad applications in materials science. However, existing generative models struggle to produce comple…
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…