Using AI to aid automation of proof search in Formal Methods

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.

Read more »

News, events & publications

AI4FM 2015 programme published!

The programme and venue information of the upcoming AI4FM 2015 workshop has been published. We are looking forward to welcoming all attendees and having a productive workshop!

Posted on 28 August 2015

Capturing Proof Process

Andrius Velykis. Capturing Proof Process. PhD thesis, School of Computing Science, Newcastle University, UK, 2015.

A PhD thesis by Andrius Velykis, developed as part of the AI4FM project, is now available. Andrius’ PhD thesis investigates capture, abstraction and inferring of interactive proof processes. The captured data can be used to extract reusable proof strategies as well as improve proof maintenance, teaching and training, etc. Associated tools, namely the ProofProcess framework, are available on GitHub.

Posted on 11 July 2015

AI4FM 2015

The 6th International Workshop on the use of AI in Formal Methods (AI4FM 2015) will take place on the 1st of September, 2015 in Edinburgh, Scotland, colocated with AVoCS’15.

We encourage to submit short contributions to present at the workshop. Submission deadline is 1st August 2015. Please see the call for papers for more details.

Leo Freitas, Cliff B. Jones, Andrius Velykis, and Iain Whiteside. A model for capturing and replaying proof strategies. In Dimitra Giannakopoulou and Daniel Kroening, editors, VSTTE 2014, volume 8471 of LNCS, pages 183–199. Springer, 2014.

Publication added on 10 April 2015

Gudmund Grov, Aleks Kissinger, and Yuhui Lin. Tinker, tailor, solver, proof. In Christoph Benzmüller and Bruno Woltzenlogel Paleo, editors, UITP 2014, volume 167 of EPTCS, pages 23–34, 2014.

Publication added on 10 April 2015

Ewen Denney, Ganesh J. Pai, and Iain Whiteside. Formal foundations for hierarchical safety cases. In HASE 2015, pages 52–59. IEEE, 2015.

Publication added on 10 April 2015

News archive

Mailing list

AI4FM project e-mail list is available at JISC:


Grant information