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.
The fourth workshop in the AI4FM series (AI4FM 2013) will be held as a satellite event of ITP 2013, on 22nd July 2013 in Rennes, France. If you would like to attend, then please submit a short abstract to email@example.com by 20 April.
We welcome Iain Whiteside, who is joining AI4FM project as a Research Associate at Newcastle University. He is replacing Leo Freitas, who took a position of Lecturer at Newcastle University and will continue his involvement in AI4FM as project’s Co-Investigator.
Posted on 20 February 2013
Seminar: A graphical strategy language to enable proof re-use
On 13 September 2012 by Gudmund Grov at Oxford University, OASIS: The Oxford Advanced Seminar on Informatic Structures seminar series.
Talk posted on 12 February 2013
Andrew Ireland, Gudmund Grov, Maria Teresa Llano, and Michael Butler. Reasoned modelling critics: Turning failed proofs into modelling guidance. Science of Computer Programming, 78(3):293–309, 2013. Special issue: Abstract State Machines, Alloy, B and Z – Selected Papers from ABZ 2010.
Publication added on 10 February 2013
We are pleased to inform you that the report of Dagstuhl seminar 12271 ‘AI meets Formal Software Development’ is now published as part of the periodical Dagstuhl Reports. The report is available online at http://dx.doi.org/10.4230/DagRep.2.7.1.
The seminar report features abstracts of most of the talks given at the seminar plus an executive summary by Cliff Jones.
Posted on 01 February 2013
Alan Bundy, Dieter Hutter, Cliff B. Jones, and J Strother Moore. AI meets Formal Software Development (Dagstuhl Seminar 12271). Dagstuhl Reports, 2(7):1–29, 2012.
Publication added on 01 February 2013
AI4FM project e-mail list is available at JISC: