Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Alexandria: A Tool for Hierarchical Verification

Annette BunkerContact Information, Trent N. LarsonContact Information, Michael D. JonesContact Information and Phillip J. WindleyContact Information

(6)  University of Utah, USA
(7)  Brigham Young University, Provo, UT 84602-6576
Abstract
Alexandria is an implementation of the hierarchical verification methodology for the Higher-Order Logic (HOL) theorem prover. The main contribution of Alexandria is the reduction of e.ort required by the user to create and use hierarchical hardware proofs in HOL. We discuss the implementation and use of Alexandria with an example and outline our future work.
Thiswork was sponsored by the National Science Foundation under NSF grant MIP-9412581

Contact Information Annette Bunker
Email: bunker@cs.byu.edu

Contact Information Trent N. Larson
Email: larson@cs.byu.edu

Contact Information Michael D. Jones
Email: mjones@cs.utah.edu

Contact Information Phillip J. Windley
Email: windley@cs.byu.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.106 • Server: mpweb19
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)