EPSRC logo

Details of Grant 

EPSRC Reference: GR/N64571/01
Title: A PROOF SYSTEM FOR CORRECT PROGRAM DEVELOPMENT
Principal Investigator: Fourman, Professor MP
Other Investigators:
Fleuriot, Dr J Fleuriot, Dr J
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:
Information Technologies
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