| EPSRC Reference: |
EP/H024050/1 |
| Title: |
AI4FM: using AI to aid automation of proof search in Formal Methods |
| Principal Investigator: |
Jones, Professor CB |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing Sciences |
| Organisation: |
Newcastle University |
| Scheme: |
Standard Research |
| Starts: |
01 April 2010 |
Ends: |
30 September 2014 |
Value (£): |
467,296
|
| EPSRC Research Topic Classifications: |
| Artificial Intelligence |
Fundamentals of Computing |
| Software Engineering |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
15 Dec 2009
|
ICT Prioritisation Panel (Dec 09)
|
Announced
|
|
|
Summary on Grant Application Form |
|
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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ncl.ac.uk |