| Computer Science Laboratory | |
| Contact | |
 | People at CSL |
| Projects at CSL |
| Research Programs |
| Division Home | |
 Self-Checking Prover Study Final Report by M. J. C. Gordon, J. M. J. Herbert, R. W. S. Hale, J. Harrison, W. Wong & J. von Wright. Abstract The Self-Checking Prover Study is Task 2 of the Foundations of Secure Formal Methods project. The main goal of this task was the design and development of a prover/checker pair for the HOL theorem proving system; that is, a version of the HOL prover modified to record and output the proofs that are made in the system, and a companion checker to determine whether such proofs are logically sound.Files |
||||
About Us 
R&D Divisions
Careers
Newsroom
Contact Us
©
2025 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy