AI4FM project e-mail list is available at JISC: ai4fm-info@jiscmail.ac.uk
AI4FM project overview
AI4FM project aims to use "learning" techniques from artificial intelligence to record and abstract how experts do proofs in order to increase the proportion of cases where proofs are constructed without (or with minimal) human intervention. AI4FM is an EPSRC-funded research project, a joint effort between Newcastle, Edinburgh and Heriot-Watt universities.
Most formal methods give rise to proof obligations (POs). Most of the POs are discharged by automatic theorem provers, however some of them (typically 5-20%) still require guidance from a proof expert. Manually finding a proof can be a difficult process, and is often a bottleneck in industrial applications of formal methods. However, once a proof is found,
many other POs can be discharged by following the same proof pattern. The goal of AI4FM is to automatically discharge POs of "similar form" by exploring the extra information provided from the expert provided proof attempt.
News & events
-
14 November 2011
Upcoming event: Dagstuhl seminar ‘AI meets Formal Software Development’
A Dagstuhl seminar ‘AI meets Formal Software Development’ (Seminar 12271) related to the AI4FM project will held on 1-6 July 2012.
-
4 November 2011
Upcoming seminar: Reasoned modelling: towards decision support for system designers
Andrew Ireland will give the BCS-FACS Evening Seminar, which is joint with the London Mathematical Society in London, UK on 30 November 2011. The event is open to everyone and free to all.
-
4 November 2011
Recent publications and talk slides
A MSc thesis has been completed within the topics of AI4FM project: "Extending the proof methods and critics of a proof planner" by Daniel Raggi. The thesis is available on the website.
Ideas about inferring the proof process from an expert have been presented during a IFIP WG 2.3 meeting. The slides are available for download.
