SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

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
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy