Techniques for Automatic Deduction
Abstract
This report covers progress on a 2-year research effort toward the development of new theorem-proving methods for program verification, and the empirical investigation of these methods in actual verification systems. The research conducted during the course of the project focused on methods for simplifying formulas of the kind that arise frequently in the verification of programs. The importance of simplification methods, as opposed to pure proof methods, was pointed up by verification work conducted under a previous AFOSR contract. Perhaps the most significant outcome of the project is the development of an experimental theorem prover that has been used extensively in the proof of correctness of the design of a fault-tolerant operating system developed under NASA support. We believe that the technology embodied in this experimental system could be successfully applied to the development of a production verification system. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1981
- Accession Number
- ADA108979
Entities
People
- P. M. Meliar-smith
- Richard L. Schwartz
- Robert E. Shostak
Organizations
- SRI International