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.

Read more »

News & events

  • PhD position available in Edinburgh

    A PhD position is available within AI4FM project at the School of Informatics in the University of Edinburgh. The student will be supervised by Alan Bundy and Gudmund Grov.

    The projected PhD task is to analyse ways in which proof attempts fail and are subsequently repaired. This analysis will result in a generic strategy language for describing and classifying failure and repair. The strategy language would be used to describe how experts recover from failure and to guide automated proof search.

    Learn more and apply »

  • 4 August 2010

    Upcoming talk: Formal Modelling of Separation Kernel Components

    A research paper "Formal Modelling of Separation Kernel Components" will be presented at ICTAC 2010 conference, Natal, Brazil, on 2 September 2010.

    View the publication »
    View the talk information »

  • 15 July 2010

    Publication text and talk slides for AFM10 workshop

    The text and talk slides of "Ideas for a high-level proof strategy language" publication for AFM10 workshop are now available on the website.

    View the publication »
    View the talk slides »

  • 14 July 2010

    Upcoming talks at VERIFY-2010 and VSTTE 2010

    Cliff B Jones will be an invited speaker at VERIFY-2010 workshop (part of FLoC 2010) on 20 July 2010.
    Learn more »

    Gudmund Grov will give a presentation at Tools and Experiments workshop at VSTTE 2010 on 19 August 2010.
    Learn more »

News archive »