Abstract is missing.
- Introduction to the HOL SystemMichael J. C. Gordon. 2-3
- HOL Around the WorldSara Kalvala. 4-12
- Dealing With Temporal Complexity in Hardware VerificationJohn Herbert. 13-21
- Verifying Arithmetic Hardware in Higher-Order LogicShiu-Kai Chin. 22-31
- The Practical Verification of Microprocessor DesignsPhillip J. Windley. 32-37
- Verification of Integrated SubsystemsE. Thomas Schubert. 38-51
- Reasoning About SoftwareRoger Hale. 52-58
- On the use of the HOL system for Protocol VerificationRachel Cardell-Oliver. 59-62
- Mechanizing Security in HOLWilliam L. Harrison, Karl N. Levitt. 63-66
- Learning to use HOLPaul Loewenstein. 67-74
- The Need for Formal Verification in Hardware Design and What Formal Verification Has Not Done for Me LatelyKurt Keutzer. 77-86
- Verification of Composed Hardware Systems Using CCSE. Thomas Schubert. 88-95
- An HOL Theory for Logic States with Indeterminate StrengthsJ. W. Gambles, Phillip J. Windley. 96-103
- Formalization of VHDL Synthesis Procedure in Higher-Order LogicX. Wang, Edward P. Stabler. 106-120
- Implementing and Verifying Finite-State Machines Using Types in Higher-Order LogicShiu-Kai Chin, Graham M. Birtwistle. 121-129
- Industrial Application of Theorem Proving to System Level DesignSimon Bainbridge, Albert John Camilleri, Roger Fleming. 130-142
- Implementing a Real-Time Process Algebra in HOLRichard Gerber, Elsa L. Gunter, Insup Lee. 144-154
- Mechanising the Temporal Logic of Actions in HOLJoakim von Wright. 155-159
- Using HOL to produce custom verification toolsD. Shepherd. 162-169
- Integrating a First-Order Automatic Prover in the HOL EnvironmentRamayya Kumar, Thomas Kropf, Klaus Schneider. 170-176
- Window Inference in the HOL SystemJim Grundy. 177-189
- First Steps Towards Automating Hardware Proofs in HOLRamayya Kumar, Thomas Kropf, Klaus Schneider. 190-193
- Design Choices in Specification Languages and Verification SystemsJohn M. Rushby. 195-204
- Mechanizing Program Verification in HOLSten Agerholm. 208-222
- Proof of Program TransformationsRachel E. O. Roxas, Malcolm C. Newey. 223-230
- Program Transformations and Refinements in HOLJoakim von Wright, Kaisa Sere. 231-239
- Case Studies in Compiler Correctness Using HOLDavid F. Martin, R. J. Toal. 242-252
- A Verified Compiler for a Structured Assembly LanguagePaul Curzon. 253-262
- A Report on ICL HOLR. D. Arthan. 280-283
- PM: A Proof Manager for HOL and Other ProversGeorge Fink, Myla Archer, Lie Yang. 286-304
- Developing an Interface for HOLSara Kalvala. 305-317
- An Informal Discussion of Issues in Mechanically-Assisted ReasoningMatt Kaufmann. 318-337
- Formal Hardware Verification in HOL and in Boyer-Moore: A Comparative AnalysisCatia M. Angelo, Diederik Verkest, Luc J. M. Claesen, Hugo De Man. 340-347
- A Package for Inductive Relation Definitions in HOLThomas F. Melham. 350-357
- Defining Recursive Functions in HOLW. Ploegaerts, Luc J. M. Claesen, Hugo De Man. 358-366
- Recursive Boolean Functions in HOLFlemming Andersen, Kim Dam Petersen. 367-377
- Proof Based ComputationMalcolm C. Newey. 380-383
- Reasoning about Petri Nets in HOLE. de Barros Lucena. 384-394
- A Simple Graph Theory and Its Application in Railway SignallingW. Wong. 395-409