AI4FM: using AI to aid automation of proof search in Formal Methods

Lead Research Organisation: University of Edinburgh
Department Name: Sch of Informatics

Abstract

Formal Methods bring to software engineering the level of scientific underpinning familiar in other engineering disciplines. Such methods use specification languages with precise meaning and thus open the possibility of proving that a design (ultimately the implementation) satisfies the specification.Such formal methods have come a long way since their inception and they are now used in applications far more common than the safety-critical systems where they were first deployed. Significant awareness of their potential has come from the use of push-button, post facto, methods that derive from ideas of model checking . The family of methods that can be thought of as top-down have more potential pay-off but are also more challenging for users. Any post-facto method has to face the prospect of incorrect programs - extracting their specifications can be unedifying. Furthermore, an enormous amount of the waste in software development derives from scrap and rework when design errors are discovered after their insertion (but possibly before there is even code to execute). Both post-facto and top-down approaches are important: we choose to address the latter and tackle a key cost in their deployment.In justifying a top-down step of design, the user has to discharge so-called proof obligations . These are small proofs that can often be discharged by an automatic theorem prover. But where they are not discharged automatically, an engineer is faced with the unfamiliar task of constructing a formal proof. Improvements in so-called heuristics can help increase the power of theorem provers. This 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.

Publications

10 25 50

publication icon
Freitas L (2013) Formalizing workflows partitioning over federated clouds: multi-level security and costs in International Journal of Computer Mathematics

publication icon
Grov G (2017) The Tinker tool for graphical tactic development in International Journal on Software Tools for Technology Transfer

publication icon
Grov G (2014) Tinker, tailor, solver, proof in Electronic Proceedings in Theoretical Computer Science

publication icon
Grov, G (2010) A small experiment in Event-B rippling in Proceedings of AVoCS 2010 and Rodin User and Developer Workshop 2010

publication icon
Jones, CB (2010) Ideas for a high-level proof strategy language in 5th Automated Formal Methods workshop (AFM'10)

publication icon
Lin Y (2012) NASA Formal Methods

publication icon
Lin Y (2019) Automating Event-B invariant proofs by rippling and proof patching in Formal Aspects of Computing

 
Description Please see the details on the grant EP/H024050/1 - this is the grant owned by the lead site at Newcastle.
Exploitation Route Please see the details on the grant EP/H024050/1 - this is the grant owned by the lead site at Newcastle.
Sectors Other

 
Description Please see the details on the grant EP/H024050/1 - this is the grant owned by the lead site at Newcastle.