| EPSRC Reference: |
GR/H40570/01 |
| Title: |
COMBINING HOL WITH ISABELLE |
| Principal Investigator: |
Paulson, Professor LC |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 September 1992 |
Ends: |
31 August 1995 |
Value (£): |
122,431
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
To exercise the technology underlying the theorem-prover 'Isabelle' on major hardware/system verifications. To investigate how Isabelle compares to HOL as an environment for large proofs. To examine the use of Isabelle as an application-oriented verification environment.Progress:The first part of the work involved comparing proofs in HOL and Isabelle. We have chosen the proofs of correctness of two hardware circuits (a parity checker and a multiplier) already described in HOL and translated them as closely as possible into Isabelle. Other examples included conjectures arising from the specification of a nuclear reactor (due to David Parnas) and theorems about Greatest Common Divisors.All these verification problems were performed in Isabelle, and they supplied us with some comparisons as to how the more applications-oriented users view the proof process. For example, the hardware proofs involve the extensive use of rewriting; much work was invested in improving the efficiency of Isabelle's simplifier, so that now it is as fast as HOL's (and considerably more powerful).We hoped Isabelle would be particularly successful at embedding different application formalisms. We have done three different experiments along these lines; the main one concerns Lamport's Temporal Logic of Actions (TLA).Leslie Lamport developed TLA for reasoning about timing properties of concurrent programs. We have implemented TLA in Isabelle, following the calculus and mode of use described in Lamport's paper. The resulting proof system is quite usable, with few changes to the methodology and representation. We have found that Isabelle's tools (particularly the flexible parser and pretty-printing) indeed facilitate the development of embeddings. Work on TLA is continuing; we aim to perform proofs of published examples. We are also looking for other ways to improve Isabelle's support for natural and direct embeddings.
|
|
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.cam.ac.uk |