the use of AI to automate proof search in Formal Methods

AI4FM

 

Grant information 

GRANT number

     EPSRC EH/H024050

start date

     1 April 2010

duration 

     4 years

Primary investigators 

     Cliff B Jones (University of Newcastle)

     Alan Bundy (University of Edinburgh)

CO-Investigator 

     Andrew Ireland (Heriot-Watt University)

research Associative  

    Gudmund Grov (University of Edinburgh)

COnsultant

    Michael Butler (University of Southampton)

other funding

    EPSRC platform grant EP/E005713/1

    EPSRC platform grant EP/E035329/1

Overview of AI4FM

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.

 

Partners


AI4FM is a joint project between University of Newcastle, University of Edinburgh, Heriot-Watt University and University of Southampton. The following people are involved

  1. •Cliff B Jones (Newcastle)

  2. •Alan Bundy (Edinburgh)

  3. •Andrew Ireland (Heriot-Watt)

  4. •Gudmund Grov (Edinburgh)

  5. •Michael Butler (Southampton)