EPSRC logo

Details of Grant 

EPSRC Reference: GR/H40570/01
Title: COMBINING HOL WITH ISABELLE
Principal Investigator: Paulson, Professor LC
Other Investigators:
Gordon, Professor M
Researcher Co-investigators:
Project Partners:
Department: Computer Laboratory
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
No information has been submitted for this grant.
Potential use in non-academic contexts
No information has been submitted for this grant.
Impacts
No information has been submitted for this grant.
Sectors submitted by the Researcher
No information has been submitted for this grant.
Project URL:  
Further Information:  
Organisation Website: http://www.cam.ac.uk