AI4FM

Using AI to aid automation of proof search in Formal Methods

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

Leo Freitas and Iain Whiteside. Proof patterns for formal methods. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014, volume 8442 of LNCS, pages 279–295. Springer, 2014.

Publication added on 10 April 2015

Gudmund Grov, Leo Freitas and Iain Whiteside, editors. Contribution of the AI4FM 2014 Workshop, Singapore, 2014. Department of Computer Science, Heriot-Watt University. Technical report HW-MACS-TR-0100.

Publication added on 08 May 2014

Leo Freitas, Cliff B. Jones, and Andrius Velykis. Can a system learn from interactive proofs? In Andrei Voronkov and Margarita Korovina, editors, HOWARD-60. A Festschrift on the Occasion of Howard Barringer’s 60th Birthday, pages 124-139. EasyChair, 2014.

Publication added on 20 February 2014

AI4FM 2014

AI4FM 2014 will take place as a satellite workshop of FM2014 in Singapore on 12th May 2014

Jonathan Heras, Ekaterina Komendantskaya, Moa Johannson and Ewen Maclean. Proof-Pattern Recognition and Lemma Discovery in ACL2. In Logic for Programming Artificial Intelligence and Reasoning, LPAR-19th, in Stellenbosch, South Africa.

Publication added on 14 November 2013

Gudmund Grov, Aleks Kissinger and Yuhui Lin. A Graphical Language for Proof Strategies. In Logic for Programming Artificial Intelligence and Reasoning, LPAR-19th, in Stellenbosch, South Africa.

Publication added on 14 November 2013

Leo Freitas, Cliff B. Jones, Andrius Velykis, and Iain Whiteside. How to say why (in AI4FM). Technical Report CS-TR-1398, School of Computing Science, Newcastle University, October 2013.

Publication added on 13 November 2013

Cliff B. Jones, Leo Freitas, and Andrius Velykis. Ours is to reason why. In Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors, Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of LNCS, pages 227–243, Shanghai, China, September 2013. Springer.

Publication added on 12 November 2013

Proceedings of AI4FM 2013 workshop are now available

The 4th international workshop on Artificial Intelligence for Formal Methods (AI4FM 2013) has been held as a satellite event of the 4th conference on Interactive Theorem Proving (ITP 2013) in Rennes, France on 22 July 2013.

AI4FM 2013 workshop has brought together researchers from formal methods and AI; it explored the issue of how AI can be used to support the formal software development process, including modelling and proof.

The workshop consisted of one invited talk: Sharing the Burden of (Dis)proof with Nitpick and Sledgehammer by Jasmin Blanchette, and 9 regular talks. The abstracts of regular talks have been published as a Heriot-Watt Computer Science Technical Report.

Further information about AI4FM 2013 is available in the workshop website.

Gudmund Grov, Ewen Maclean, and Leo Freitas, editors. Contributions to AI4FM 2013, Rennes, France, 2013. Department of Computer Science, Heriot-Watt University. Technical report HW-MACS-TR-0100.

Publication added on 01 August 2013

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.

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.

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

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.

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

Gudmund Grov, Andrew Ireland, and Maria Teresa Llano. Refinement plans for informed formal design. In John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, volume 7316 of LNCS, pages 208–222. Springer, 2012.

Publication added on 20 December 2012

Talk: A statistical relational learning challenge – extracting proof strategies from exemplar proofs

On 30 June 2012 by Gudmund Grov at ICML-12 Workshop on Statistical Relational Learning (SRL 2012), Edinburgh, Scotland.

Talk posted on 20 December 2012

Gudmund Grov, Ekaterina Komendantskaya, and Alan Bundy. A statistical relational learning challenge – extracting proof strategies from exemplar proofs. In ICML-12 Workshop on Statistical Relational Learning (SRL 2012), Edinburgh, Scotland, June 2012.

Publication added on 20 December 2012

Iain Whiteside, David Aspinall, and Gudmund Grov. An essence of SSReflect. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Conferences on Intelligent Computer Mathematics—CICM 2012, volume 7362 of LNCS, pages 186–201. Springer, 2012.

Publication added on 20 December 2012

Iain Whiteside, David Aspinall, Lucas Dixon, and Gudmund Grov. Towards formal proof script refactoring. In James H. Davenport, William M. Farmer, Josef Urban, and Florian Rabe, editors, Intelligent Computer Mathematics—18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, volume 6824 of LNCS, pages 260–275. Springer, 2011.

Publication added on 20 December 2012

Ewen Maclean is joining AI4FM Edinburgh team!

We welcome Ewen Maclean, who is joining AI4FM project as a Research Associate at the University of Edinburgh. He is replacing Gudmund Grov, who is moving to Heriot-Watt University to continue his research in AI4FM as project’s Co-Investigator.

Posted on 21 August 2012

Talk: Inferring the Proof Process (Upcoming)

On 27 August 2012 by Andrius Velykis at Doctoral Symposium at 18th International Symposium on Formal Methods (FM2012), Paris, France.

Talk posted on 21 August 2012 (updated 13 February 2013: added talk slides)

Andrius Velykis. Inferring the Proof Process. In Christine Choppy, David Delayahe, and Kaïs Klaï, editors, Doctoral Symposium at 18th International Symposium on Formal Methods (FM2012), Paris, France, August 2012.

Publication added on 21 August 2012

AI4FM talks in Dagstuhl seminar ‘AI meets Formal Software Development’

Copies of slides from the AI4FM talks presented at Dagstuhl seminar ‘AI meets Formal Software Development’ are now also available on this website. This is a subset of all talks given at the seminar. As mentioned before, slides and abstracts of most of the talks are available in the seminar information page.

Talk: The use of Rippling to automate Event-B invariant preservation proofs

On 30 June 2012 by Yuhui Lin at IJCAR Workshop on Automated Theory eXploration (ATX 2012), Manchester, UK.

Talk posted on 21 August 2012

Yuhui Lin, Alan Bundy, and Gudmund Grov. The use of Rippling to automate Event-B invariant preservation proofs. In IJCAR Workshop on Automated Theory eXploration (ATX 2012), Manchester, UK, June 2012.

Publication added on 21 August 2012

Talk: The use of Rippling to automate Event-B invariant preservation proofs

On 05 April 2012 by Yuhui Lin at 4th NASA Formal Methods Symposium (NFM 2012), Norfolk, Virginia, USA.

Talk posted on 21 August 2012

Yuhui Lin, Alan Bundy, and Gudmund Grov. The use of Rippling to automate Event-B invariant preservation proofs. In Alwyn Goodloe and Suzette Person, editors, NASA Formal Methods—4th International Symposium, NFM 2012, volume 7226 of LNCS, pages 231–236. Springer, 2012.

Publication added on 21 August 2012