default search action
4th TPHOLs 1991: Davis, CA, USA
- Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley:
Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA. IEEE Computer Society 1992
Tutorial Papers
- Michael J. C. Gordon:
Introduction to the HOL System. TPHOLs 1991: 2-3 - Sara Kalvala:
HOL Around the World. TPHOLs 1991: 4-12 - John Herbert:
Dealing With Temporal Complexity in Hardware Verification. TPHOLs 1991: 13-21 - Shiu-Kai Chin:
Verifying Arithmetic Hardware in Higher-Order Logic. TPHOLs 1991: 22-31 - Phillip J. Windley:
The Practical Verification of Microprocessor Designs. TPHOLs 1991: 32-37 - E. Thomas Schubert:
Verification of Integrated Subsystems. TPHOLs 1991: 38-51 - Roger Hale:
Reasoning About Software. TPHOLs 1991: 52-58 - Rachel Cardell-Oliver:
On the use of the HOL system for Protocol Verification. TPHOLs 1991: 59-62 - William L. Harrison, Karl N. Levitt:
Mechanizing Security in HOL. TPHOLs 1991: 63-66 - Paul Loewenstein:
Learning to use HOL. TPHOLs 1991: 67-74
Workshop Papers
- Kurt Keutzer:
The Need for Formal Verification in Hardware Design and What Formal Verification Has Not Done for Me Lately. TPHOLs 1991: 77-86 - E. Thomas Schubert:
Verification of Composed Hardware Systems Using CCS. TPHOLs 1991: 88-95 - J. W. Gambles, Phillip J. Windley:
An HOL Theory for Logic States with Indeterminate Strengths. TPHOLs 1991: 96-103 - X. Wang, Edward P. Stabler:
Formalization of VHDL Synthesis Procedure in Higher-Order Logic. TPHOLs 1991: 106-120 - Shiu-Kai Chin, Graham M. Birtwistle:
Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic. TPHOLs 1991: 121-129 - Simon Bainbridge, Albert John Camilleri, Roger Fleming:
Industrial Application of Theorem Proving to System Level Design. TPHOLs 1991: 130-142 - Richard Gerber, Elsa L. Gunter, Insup Lee:
Implementing a Real-Time Process Algebra in HOL. TPHOLs 1991: 144-154 - Joakim von Wright:
Mechanising the Temporal Logic of Actions in HOL. TPHOLs 1991: 155-159 - David Shepherd:
Using HOL to produce custom verification tools. TPHOLs 1991: 162-169 - Ramayya Kumar, Thomas Kropf, Klaus Schneider:
Integrating a First-Order Automatic Prover in the HOL Environment. TPHOLs 1991: 170-176 - Jim Grundy:
Window Inference in the HOL System. TPHOLs 1991: 177-189 - Ramayya Kumar, Thomas Kropf, Klaus Schneider:
First Steps Towards Automating Hardware Proofs in HOL. TPHOLs 1991: 190-193 - John M. Rushby:
Design Choices in Specification Languages and Verification Systems. TPHOLs 1991: 195-204 - Sten Agerholm:
Mechanizing Program Verification in HOL. TPHOLs 1991: 208-222 - Rachel E. O. Roxas, Malcolm C. Newey:
Proof of Program Transformations. TPHOLs 1991: 223-230 - Joakim von Wright, Kaisa Sere:
Program Transformations and Refinements in HOL. TPHOLs 1991: 231-239 - David F. Martin, R. J. Toal:
Case Studies in Compiler Correctness Using HOL. TPHOLs 1991: 242-252 - Paul Curzon:
A Verified Compiler for a Structured Assembly Language. TPHOLs 1991: 253-262 - Jim Alves-Foss, Karl N. Levitt:
Mechanical Verification of Secure Distributed Systems in Higher Order Logic. TPHOLs 1991: 263-278 - R. D. Arthan:
A Report on ICL HOL. TPHOLs 1991: 280-283 - George Fink, Myla Archer, Lie Yang:
PM: A Proof Manager for HOL and Other Provers. TPHOLs 1991: 286-304 - Sara Kalvala:
Developing an Interface for HOL. TPHOLs 1991: 305-317 - Matt Kaufmann:
An Informal Discussion of Issues in Mechanically-Assisted Reasoning. TPHOLs 1991: 318-337 - Catia M. Angelo, Diederik Verkest, Luc J. M. Claesen, Hugo De Man:
Formal Hardware Verification in HOL and in Boyer-Moore: A Comparative Analysis. TPHOLs 1991: 340-347 - Thomas F. Melham:
A Package for Inductive Relation Definitions in HOL. TPHOLs 1991: 350-357 - W. Ploegaerts, Luc J. M. Claesen, Hugo De Man:
Defining Recursive Functions in HOL. TPHOLs 1991: 358-366 - Flemming Andersen, Kim Dam Petersen:
Recursive Boolean Functions in HOL. TPHOLs 1991: 367-377 - Malcolm C. Newey:
Proof Based Computation. TPHOLs 1991: 380-383 - E. de Barros Lucena:
Reasoning about Petri Nets in HOL. TPHOLs 1991: 384-394 - W. Wong:
A Simple Graph Theory and Its Application in Railway Signalling. TPHOLs 1991: 395-409
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.