Overview - AI4FM

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.

AI4FM 2013: call for papers

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 ai4fm2013@ai4fm.org by 20 April.

For more details see the call for papers and the AI4FM 2013 workshop website.

View call for papers Workshop website

Posted on 22 February 2013

Iain Whiteside is joining AI4FM Newcastle team!

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.

View AI4FM people

Posted on 20 February 2013

View

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

Read

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

Summary report for Dagstuhl seminar ‘AI meets Formal Software Development’ is now available

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.

View seminar report

Posted on 01 February 2013

Read

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

News archive