A Generic Proof Checker

Watson, Geoffrey Norman (2001). A Generic Proof Checker PhD Thesis, School of Computer Science and Electrical Engineering, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
thesis.pdf thesis.pdf application/pdf 1.25MB 747
thesis.ps thesis.ps Click to show the corresponding preview/stream application/postscript 2.09MB 509
Author Watson, Geoffrey Norman
Thesis Title A Generic Proof Checker
School, Centre or Institute School of Computer Science and Electrical Engineering
Institution The University of Queensland
Publication date 2001-06
Thesis type PhD Thesis
Supervisor J. Welsh
P. Robinson
Total pages 304
Collection year 2002
Language eng
Subjects 280499 Computation Theory and Mathematics not elsewhere classified
280403 Logics and Meanings of Programs
700102 Application tools and system utilities
Abstract/Summary The use of formal methods in software development seeks to increase our confidence in the resultant system. Their use often requires tool support, so the integrity of a development using formal methods is dependent on the integrity of the tool-set used. Specifically its integrity depends on the theorem prover, since in a typical formal development system the theorem prover is used to establish the validity of the proof obligations incurred by all the steps in the design and refinement process. In this thesis we are concerned with tool-based formal development systems that are used to develop high-integrity software. Since the theorem prover program is a critical part of such a system, it should ideally have been itself formally verified. Unfortunately, most theorem provers are too complex to be verified formally using currently available techniques. An alternative approach, which has many advantages, is to include a proof checker as an extra component in the system, and to certify this. A proof checker is a program which reads and checks the proofs produced by a theorem prover. Proof checkers are inherently simpler than theorem provers, since they only process actual proofs, whereas much of the code of a theorem prover is concerned with searching the space of possible proofs to find the required one. They are also free from all but the simplest user interface concerns, since their input is a proof produced by another program, and their output may be as simple as a `yes/no' reply to the question: Is this a valid proof? plus a list of assumptions on which this judgement is based. When included in a formal development system a stand-alone proof checker is, in one sense, superfluous, since it does not produce any proofs -- the theorem prover does this. Instead its importance is in establishing the integrity of the results of the system -- it provides extra assurance. A proof checker provides extra assurance simply by checking the proofs, since all proofs have then been validated by two independent programs. However a proof checker can provide an extra, and higher, level of assurance if it has been formally verified. In order for formal verification to be feasible the proof checker must be as simple as possible. In turn the simplicity of a proof checker is dependent on the complexity of the data which it processes, that is, the representation of the proofs that it checks. This thesis develops a representation of proofs that is simple and generic. The aim is to produce a generic representation that is applicable to the proofs produced by a variety of theorem provers. Simplicity facilitates verification, while genericity maximises the return on the effort of verification. Using a generic representation places obligations on the theorem provers to produce a proof record in this format. A flexible recorder/translator architecture is proposed which allows proofs to be recorded by existing theorem provers with minimal changes to the original code. The prover is extended with a recorder module whose output is then, if necessary, converted to the generic format by a separate translator program. A formal specification of a checker for proofs recorded in this representation is given. The specification could be used to formally develop a proof-checker, although this step is not taken in this thesis. In addition the characteristics of both the specification and possible implementations are investigated. This is done to assess the size and feasibility of the verification task, and also to confirm that the design is not over-sensitive to the size of proofs. This investigation shows that a checker developed from the specification will be scalable to handle large proofs. To investigate the feasibility of a system based on this architecture, prototype proof recorders were developed for the Ergo 5 and Isabelle 98 theorem provers. In addition a prototype checker was written to check proofs in the proposed format. This prototype is compatible with the formal specification. The combined system was tested successfully using existing proofs for both the Ergo 5 and Isabelle 98 theorem provers.
Keyword Software verification
theorem proving
proof checking

Document type: Thesis
Collection: UQ Theses Collection (RHD) - Open Access
 
Versions
Version Filter Type
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 783 Abstract Views, 1262 File Downloads  -  Detailed Statistics
Created: Fri, 02 Apr 2004, 10:00:00 EST by G N Watson on behalf of Research Management Office