### Skapa referens, olika format (klipp och klistra)

**Harvard**

Davis, J. och Myreen, M. (2015) *The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)*.

** BibTeX **

@article{

Davis2015,

author={Davis, J. and Myreen, Magnus O.},

title={The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)},

journal={Journal of automated reasoning},

issn={0168-7433},

volume={55},

issue={2},

pages={117-183},

abstract={This paper presents, we believe, the most comprehensive evidence of a theorem prover’s soundness to date. Our subject is the Milawa theorem prover. We present evidence of its soundness down to the machine code. Milawa is a theorem prover styled after NQTHM and ACL2. It is based on an idealised version of ACL2’s computational logic and provides the user with high-level tactics similar to ACL2’s. In contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat like an LCF-style system. We explain how the Milawa theorem prover is constructed as a sequence of reflective extensions from its kernel. The kernel establishes the soundness of these extensions during Milawa’s bootstrapping process. Going deeper, we explain how we have shown that the Milawa kernel is sound using the HOL4 theorem prover. In HOL4, we have formalized its logic, proved the logic sound, and proved that the source code for the Milawa kernel (1,700 lines of Lisp) faithfully implements this logic. Going even further, we have combined these results with the x86 machine-code level verification of the Lisp runtime Jitawa. Our top-level theorem states that Milawa can never claim to prove anything that is false when it is run on this Lisp runtime.},

year={2015},

keywords={Machine code, Proof assistant, Soundness, Theorem proving },

}

** RefWorks **

RT Journal Article

SR Electronic

ID 221523

A1 Davis, J.

A1 Myreen, Magnus O.

T1 The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)

YR 2015

JF Journal of automated reasoning

SN 0168-7433

VO 55

IS 2

SP 117

OP 183

AB This paper presents, we believe, the most comprehensive evidence of a theorem prover’s soundness to date. Our subject is the Milawa theorem prover. We present evidence of its soundness down to the machine code. Milawa is a theorem prover styled after NQTHM and ACL2. It is based on an idealised version of ACL2’s computational logic and provides the user with high-level tactics similar to ACL2’s. In contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat like an LCF-style system. We explain how the Milawa theorem prover is constructed as a sequence of reflective extensions from its kernel. The kernel establishes the soundness of these extensions during Milawa’s bootstrapping process. Going deeper, we explain how we have shown that the Milawa kernel is sound using the HOL4 theorem prover. In HOL4, we have formalized its logic, proved the logic sound, and proved that the source code for the Milawa kernel (1,700 lines of Lisp) faithfully implements this logic. Going even further, we have combined these results with the x86 machine-code level verification of the Lisp runtime Jitawa. Our top-level theorem states that Milawa can never claim to prove anything that is false when it is run on this Lisp runtime.

LA eng

DO 10.1007/s10817-015-9324-6

LK http://dx.doi.org/10.1007/s10817-015-9324-6

OL 30