4 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…
Model-Driven Discipline for Multi-Agent LLMs: Requirement-to-Verification Generation of Traceable System Models
Ran Wei, Le Zhu, Haochi Wang +6
Software complexity is a long-standing challenge for system engineers. Model-Driven Engineering (MDE) addresses it by treating models as first-class artefacts, but a typical MDE pr…
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-…