EPSRC logo

Details of Grant 

EPSRC Reference: GR/M32443/01
Title: UNIFYING PROOF PLANS AND SCHEMAS FOR PROGRAM SYNTHESIS AND TRANSFORMATION
Principal Investigator: Bundy, Professor A
Other Investigators:
Lau, Dr K
Researcher Co-Investigators:
Project Partners:
Department: Sch of Informatics
Organisation: University of Edinburgh
Scheme: Standard Research (Pre-FEC)
Starts: 01 January 1999 Ends: 30 June 2000 Value (£): 4,020
EPSRC Research Topic Classifications:
Artificial Intelligence
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:  
Summary on Grant Application Form
The development of provably correct software and hardware systems is an important area of study, since mistakes in such systems can be extremely expensive or dangerous. Program systhesis and program transformation are fundermental tools for the development of correct computer programs. Previous research has found that program synthesis and transformation techniques must be heavily automated in order to be useful. One means of automating these techniques is the use of program schemas, which express transformation or synthesis steps using program patterns (FLO97a, FLO97b, BF97). Another approach is to formalise the synthesis or transformation stepsas theorum providing tasksand employ techniques from automated theorem proving. Proof planning (Bun88) is one such automated proof technique with promises to scale up to large scale problems, and which has been used for program and hardware synthesis (KBB93, Wig92, ASG97, CO97) and program transformation (Mad92, Ric95b). Proof plans consist of methods, which represent proof steps at a relatively high level of abstraction, ands cleanly splitthem into heuristic (the method itself) and logical (assosiated tactic) parts.An integrated view of proof plans and synthesis/transformation schemas will make a large body of examples of program synthesis and transformation schemas available to proof planning and encourge the large scale proof plans for solving real problems. At the same time, proof planning will permit schemas to be seperated into their heuristic and logical aspects, and provide a mechanism for satisfying the many and important proof obligations which result when the svhemas are applied.
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