Skip to main content
Conference ProceedingsOPEN ACCESS

A mechanically verified application for a mechanically verified environment

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (1993) 697 LNCS 268-279
DOI: 10.1007/3-540-56922-7_22
12Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

We have developed a verified application proved to be both effective and efficient. The application generates moves in the puzzlegame Nim and is coded in Piton, a language with a formal semantics and a compiler verified to preserve its semantics on the underlying machine. The Piton compiler is targeted to the FM9001, a recently fabricated verified microprocessor. The Nim program correctness proof makes use of the language semantics that the compiler is proved to implement. Like the Piton compiler proof and FM9001 design proof, the Nim correctness proof is generated using Nqthm, a proof system sometimes known as the Boyer-Moore theorem prover.

Cite

CITATION STYLE

APA

Wilding, M. (1993). A mechanically verified application for a mechanically verified environment. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 697 LNCS, pp. 268–279). Springer Verlag. https://doi.org/10.1007/3-540-56922-7_22

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free