loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Methods in Computer Aided Design (FMCAD'06)
An Integration of HOL and ACL2
San Jose, California, USA
November 12-November 16
ISBN: 0-7695-2707-8
ASCII Text
x 
 
Michael J.C. Gordon, James Reynolds, Warren A. Hunt, Matt Kaufmann, "An Integration of HOL and ACL2," Formal Methods in Computer Aided Design, pp. 153-160, Formal Methods in Computer Aided Design (FMCAD'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/FMCAD.2006.6,
author = {Michael J.C. Gordon and James Reynolds and Warren A. Hunt and Matt Kaufmann},
title = {An Integration of HOL and ACL2},
journal ={Formal Methods in Computer Aided Design},
volume = {0},
year = {2006},
isbn = {0-7695-2707-8},
pages = {153-160},
doi = {http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.6},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Formal Methods in Computer Aided Design
TI - An Integration of HOL and ACL2
SN - 0-7695-2707-8
SP153
EP160
A1 - Michael J.C. Gordon,
A1 - James Reynolds,
A1 - Warren A. Hunt,
A1 - Matt Kaufmann,
PY - 2006
KW - null
VL - 0
JA - Formal Methods in Computer Aided Design
ER -
 
Michael J.C. Gordon, University of Cambridge Computer Laboratory, UK
James Reynolds, University of Cambridge Computer Laboratory, UK
Warren A. Hunt, Department of Computer Sciences, USA
Matt Kaufmann, Department of Computer Sciences, USA
A link between the ACL2 and HOL4 proof assistants is described. This allows each system to be deployed smoothly within a single formal development. Several applications are being considered: using ACL2's execution environment for simulating HOL models; using ACL2's proof automation to discharge HOL proof obligations; and using HOL to specify and verify properties of ACL2 functions that cannot easily be stated in the first-order ACL2 logic.

Care has been taken to ensure sound translations between the logics supported by HOL and ACL2. The initial ACL2 theory has been defined inside HOL, so that it is possible to prove mechanically that first-order ACL2 functions on S-expressions correspond to higher-order functions operating on a variety of types. The translation between the two systems operates at the level of S-expressions and is intended to handle large hardware and software models.

Citation:
Michael J.C. Gordon, James Reynolds, Warren A. Hunt, Matt Kaufmann, "An Integration of HOL and ACL2," fmcad, pp.153-160, Formal Methods in Computer Aided Design (FMCAD'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.