Proof movie — A proof with the Boyer-Moore prover
- 1 March 1993
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 5 (2) , 121-151
- https://doi.org/10.1007/bf01211302
Abstract
This paper uses the Boyer-Moore prover for developing a proof of correctness for the implementation of a very small compiler. The polished version of the proof is included as an appendix. The major intent of the paper is to describe the process of proving using an automatic theorem prover.Keywords
This publication has 8 references indexed in Scilit:
- A mechanically verified code generatorJournal of Automated Reasoning, 1989
- A mechanically verified language implementationJournal of Automated Reasoning, 1989
- Microprocessor design verificationJournal of Automated Reasoning, 1989
- An approach to systems verificationJournal of Automated Reasoning, 1989
- Kit: a study in operating system verificationIEEE Transactions on Software Engineering, 1989
- A mechanical proof of the Church-Rosser theoremJournal of the ACM, 1988
- The Vienna Development Method: The Meta-LanguageLecture Notes in Computer Science, 1978
- Correctness of a compiler for arithmetic expressionsProceedings of Symposia in Applied Mathematics, 1967