SearchBrowse

close this section of the libraryftp://lal.cs.byu.edu (24)
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/abs_theory.ps, 19920928
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/superduper.ps, 19930510
Toward a Super Duper Hardware Tactic Mark Aagaard Miriam Leeser Phil Windley May 7, 1993 EE-CEG-93-4 School of Electrical Engineering Cornell University Ithaca, NY Submitted to the HOL User's Group Meeting 1993 Toward a Super Duper Hardware Tactic Mark Aagaard Miriam Leeser Phil Windley School of
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/formal.uP.modeling.ps, 19931001
Contents 1 Introduction. 2 2 A Brief Introduction to HOL. 3 3 Formal Microprocessor Modeling. 5 3.1 Basic Types. : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 3.2 State. : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 3.3 Time. : : : :
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/gen.interp.ps, 19931001
1 A Theory of Generic Interpreters Phillip J. Windley Laboratory for Applied Logic Department of Computer Science University of Idaho Moscow ID 83843 USA e-mail: Windley@cs.uidaho.edu Phone: 208.885.6501 FAX: 208.885.6645
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/sig.val.modeling.ps, 19931206
Verification of VLSI Circuits: Signal Value Modeling and HDL Translation Jody W. Gambles Microelectronics Research Center, University of New Mexico, Albuquerque NM 87131 Phillip J. Windley Laboratory for Applied Logic, Department of Computer Science Brigham Young University Provo UT 846021
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/dysfunctional.ps, 19940105
Dysfunctional Programming: Teaching Programming using Formal Methods to Non-Computer Science Majors Michael Barnett Laboratory for Applied Logic Department of Computer Science University of Idaho Moscow, Idaho 83844-1010 mbarnett@cs.uidaho.edu Phillip Windley Department of Computer Science Brigham Young
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/make.ps, 19940321
Using Make to Manage Large Proofs Phillip J. Windley Laboratory for Applied Logic Department of Computer Science Brigham Young University Provo, Utah 84602-6576 windley@cs.byu.edu
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/pipeline.ps, 19940411
A Correctness Model for Pipelined Microprocessors Phillip J. Windley Laboratory for Applied Logic Department of Computer Science Brigham Young University Provo, UT 84602-6576 windley@cs.byu.edu Michael L. Coe Laboratory for Applied Logic Department of Computer Science University of Idaho Moscow, ID
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/archspec.ps, 19940621
Specifying Instruction{Set Architectures in HOL: A Primer Phillip J. Windley Laboratory for Applied Logic Brigham Young University Provo, Utah 84602-6576
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/git.diss.ps, 19940706
The Formal Verification of Generic Interpreters By Phillip J. Windley B.S. (University of Idaho) 1982 M.S. (University of California, Davis) 1988 Dissertation Submitted in partial satisfaction of the requirements for the degree of DOCTOR OF PHILOSOPHY in Computer Science in the Graduate Division of the
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/tam.ps, 19940706
Microprocessor Verification: A Tutorial Michael L Coe Phillip J. Windley Research Report LAL-92-10 March 16, 1994
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/AVM-1-verf.ps, 19940706
The Verification of AVM{1 Phillip J. Windley Division of Computer Science University of California, Davis Research Report CSE-90-21 July, 1990
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/iterate.ps, 19940706
1 Correctness Properties for Iterated Hardware Structures Phillip J. Windley Laboratory for Applied Logic, 3370 TMCB, Brigham Young University, Provo UT 84602 Phone: 801.378.3722, FAX: 801.378.7775, email: windley@cs.byu.edu
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/inst-comm.ps, 19940706
Instruction Set Commutivity Phillip J. Windley Laboratory for Applied Logic Department of Computer Science University of Idaho Moscow ID 83843
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/vhdl-signals.ps, 19941004
REASONING ABOUT THE VHDL STANDARD LOGIC PACKAGE SIGNAL DATA TYPE J. W. Gamblesa and P. J. Windleyb aMicroelectronics Research Center, Department of Electrical and Computer Engineering, University of New Mexico, Albuquerque, New Mexico 87131 bLaboratory for Applied Logic, Department of Computer Science,
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/coe.thesis.ps, 19941010
Results from Verifying a Pipelined Microprocessor A Thesis Presented in Partial Fulfillment of the Requirements for the Degree of Master of Science with a Major in Computer Science in the College of Graduate Studies University of Idaho by Michael L. Coe October 9, 1994 Major Professor: Phillip J.
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/dec.ps, 19960131
A Brief Introduction to Formal Methods Paul E. Black Kelly M. Hall Michael D. Jones Trent N. Larson Phillip J. Windley Laboratory for Applied Logic Brigham Young University info-lal@lal.cs.byu.edu
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/hol95.ps, 19960131
Automatically Synthesized Term Denotation Predicates: A Proof Aid Paul E. Black and Phillip J. Windley Computer Science Department, Brigham Young University, Provo UT 84602, USA
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/correct.ps, 19960131
Verifying Pipelined Microprocessors Phillip J. Windley Laboratory for Applied Logic Department of Computer Science Brigham Young University Provo, Utah 84602-6576 windley@cs.byu.edu
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/ghdl.eval.ps, 19971001
Toward GHDL EVAL : A Framework for Deeply Embedding Simple HDLs in HOL Michael D. Jones, Trent N. Larson and Phillip J. Windley fjones, larson, windleyg@cs.byu.edu Computer Science Department, Brigham Young University, Provo UT 84602, USA
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/first.alexandria.ps, 19971001
A Heirarchical Formal Verification Tool for Simple HDLs Annette Bunker, Michael D. Jones, Trent N. Larson and Phillip J. Windley fbunker, jones, larson, windleyg@cs.byu.edu Computer Science Department, Brigham Young University, Provo UT 84602, USA
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/hicss31.ps, 19971001
Formal Verification of Secure Programs in the Presence of Side Effects Paul E. Black Phillip J. Windley National Institute of Computer Science Department Standards and Technology Brigham Young University Gaithersburg, Maryland 20899 Provo, Utah 84602-6576 paul.black@nist.gov windley@cs.byu.edu Copyright
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/hicss30.ps, 19971001
Verifying Resilient Software P. E. Black P. J. Windley Computer Science Department Computer Science Department Brigham Young University Brigham Young University Provo UTAH 84602-6576 Provo UTAH 84602-6576 p.black@ieee.org windley@cs.byu.edu Copyright 1997 IEEE. Published in the Proceedings of the
open this document and view contentsftp://lal.cs.byu.edu/pub/hol/lal-papers/hol96.ps, 19971001
Inference Rules for Programming Languages with Side Effects in Expressions Paul E. Black and Phillip J. Windley Computer Science Department, Brigham Young University, Provo UT 84602-6576, USA