8 papers
Graph Construction and Matching for Imperative Programs using Neural and Structural Methods
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
Reusing verification artefacts requires identifying structural and semantic similarities across programs and their specifications. In this paper, we focus on graph construction as…
Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
This paper articulates a long-term research vision for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and r…
Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
Artificial intelligence systems have achieved remarkable capability in natural language processing, perception and decision-making tasks. However, their behaviour often remains opa…
Evaluating LLM-Generated ACSL Annotations for Formal Verification
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
Formal specifications are crucial for building verifiable and dependable software systems, yet generating accurate and verifiable specifications for real-world C programs remains c…
Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
Software correctness is ensured mathematically through formal verification, which involves the resources of generating formal requirement specifications and having an implementatio…
Working Document -- Formalising Software Requirements with Large Language Models
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
This draft is a working document, having a summary of nighty-four (94) papers with additional sections on Traceability of Software Requirements (Section 4), Formal Methods and Its…