| EPSRC Reference: |
GR/M32443/01 |
| Title: |
UNIFYING PROOF PLANS AND SCHEMAS FOR PROGRAM SYNTHESIS AND TRANSFORMATION |
| Principal Investigator: |
Bundy, Professor A |
| Other Investigators: |
|
| 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: |
|
| 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 |