| EPSRC Reference: |
GR/N64571/01 |
| Title: |
A PROOF SYSTEM FOR CORRECT PROGRAM DEVELOPMENT |
| Principal Investigator: |
Fourman, Professor MP |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 January 2001 |
Ends: |
30 June 2004 |
Value (£): |
197,475
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Complex computer systems are playing an increasing role in our lives, so we would like to find ways to ensure that computer programs do not contain bugs. One idea is to develop programs in mathematical way giving proofs of their correctness. This possibility has been discussed for decades, but so far it has been feasible only for small programs. If the idea is to become practicable, one needs (among other things) clean and soundly based logics that are well adapted to realistic programming languages, and tools to carry out large chunks of proofs automatically.Recent developments in theoretical computer science now allow us to give suitable program logics for the majority of commonly used features in a large family of programming languages. This puts us in a better position than ever before to attack the problem of proving software correct.In this project, we will work out the details of a sound and easy to grasp logic for most of the Standard ML language, and develop interactive tools for carrying out proofs. We will also investigate various ways of providing automated assistance, concentrating on proof planning techniques from artificial intelligence. We will evaluate our methods by means of some substantial examples.
|
|
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.ed.ac.uk |