| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf |
Automating Verification by Functional Abstraction at the System Level.  |
TPHOLs  |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Konrad Slind |
A Parameterized Proof Manager. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | John Harrison 0001 |
Binary Decision Diagrams as a HOL Derived Rule. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian T. Graham |
An Interpretation of NODEN in HOL. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter V. Homeier, David F. Martin |
Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Ching-Tsun Chou |
Mechanical Verification of Distributed Algorithms in Higher-Order Logic. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Ralf Reetz, Thomas Kropf |
Simplifying Deep Embedding: A Formalised Code Generator. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Sten Agerholm |
LCF Examples in HOL. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas F. Melham, Juanito Camilleri (eds.) |
Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Phillip J. Windley |
Specifying Instruction-Set Architectures in HOL: A Primer. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | I. S. W. B. Prasetya |
Towards a Mechanically Supported and Compositional Calculus to Design Destributed Algorithms. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Långbacka |
A HOL Formalisation of the Temporal Logic of Actions. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Luc J. M. Claesen, Michael J. C. Gordon (eds.) |
Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992 |
TPHOLs |
1993 |
DBLP BibTeX RDF |
|
| 1 | Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley (eds.) |
Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Elsa L. Gunter |
Why we can't have SML-style datatype Declarations in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Saraswati Kalvala, Myla Archer, Karl N. Levitt |
Implementation and Use of Annotations in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Joakim von Wright, Jukka Hekanaho, P. Luostarinen, Thomas Långbacka |
Mechanising some Advanced Refinement Concepts. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Paul Loewenstein |
A Formal Theory of Simulations Between Infinite Automata. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Jing Pan, Karl N. Levitt, Myla Archer, Saraswati Kalvala |
Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Phillip J. Windley |
Abstract Theories in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Konrad Slind |
Adding New Rules to an LCF-style Logic Implementation. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Richard J. Boulton |
Boyer-Moore Automation for the HOL System. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Holger Busch |
Unification Based Induction. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Garrel Pottinger |
A Classical Type Theory with Transfinite Types. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Kees G. W. Goossens |
Operational Semantics Based on Formal Symbolic Simulation. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Sreeranga P. Rajan |
Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Richard J. Boulton |
A Lazy Approach to Fully-Expansive Theorem Proving. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | John Harrison 0001 |
Constructing the real numbers in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Li-Guo Wang |
Deriving a Correct Computer. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Massimo Bombana, Patrizia Cavalloro, Giuseppe Zaza |
Specification and Formal Synthesis of Digital Circuits. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | William L. Harrison, Myla Archer, Karl N. Levitt |
A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Nancy A. Day |
A Comparison between Statecharts and State Transition Assertions. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Myla Archer, George Fink, Lie Yang |
Linking Other Theorem Provers to HOL Using PM: Proof Manager. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Ching-Tsun Chou |
A Note on Interactive Theorem Proving with Theorem Continuation Functions. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Rachel Cardell-Oliver, Roger Hale, John Herbert |
An Embedding of Timed Transition Systems in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Mark van der Voort |
Introducing well-founded function definitions in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf |
Efficient Representation and Computation of Tableau Proofs. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Mark D. Aagaard, Miriam Leeser |
A Methodology for Reusable Hardware Proofs. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Roger B. Hughes, M. D. Francis, Simon Finn, Gerry Musgrave |
Formal Tools in Tri-State Design in Busses. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Monica Nesi |
Formalizing a Modal Logic for CSS in the HOL Theorem Prover. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Kelly M. Hall, Phillip J. Windley |
Simulating Microprocessors from Formal Specifications. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Michael McAllister |
Machine Abstraction in Microprocessor Specification. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Jim Alves-Foss |
Modelling Non-Deterministic System in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Roger B. Hughes, Gerry Musgrave |
Design-Flow Graph Partitioning. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Paul Curzon |
Deriving Correctness Properties of Compiled Code. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf |
Modelling Generic Hardware Structures by Abstract Datatypes. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Ching-Tsun Chou |
A Sequent Formulation of a Logic of Predicates in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Catia M. Angelo, Luc J. M. Claesen, Hugo De Man |
The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | John Van Tassel |
A Formalisation of the VHDL Simulation Cycle. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Thomas F. Melham |
The HOL Logic Extended with Quantification over Type Variables. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
| 1 | Ramayya Kumar, Thomas Kropf, Klaus Schneider 0001 |
First Steps Towards Automating Hardware Proofs in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Michael J. C. Gordon |
Introduction to the HOL System. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | E. de Barros Lucena |
Reasoning about Petri Nets in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Joakim von Wright |
Mechanising the Temporal Logic of Actions in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | E. Thomas Schubert |
Verification of Composed Hardware Systems Using CCS. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Paul Curzon |
A Verified Compiler for a Structured Assembly Language. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Roger Hale |
Reasoning About Software. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Shiu-Kai Chin, Graham M. Birtwistle |
Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Jim Alves-Foss, Karl N. Levitt |
Mechanical Verification of Secure Distributed Systems in Higher Order Logic. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | David Shepherd |
Using HOL to produce custom verification tools. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | John Herbert |
Dealing With Temporal Complexity in Hardware Verification. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | W. Wong |
A Simple Graph Theory and Its Application in Railway Signalling. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Rachel E. O. Roxas, Malcolm C. Newey |
Proof of Program Transformations. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | E. Thomas Schubert |
Verification of Integrated Subsystems. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Richard Gerber 0001, Elsa L. Gunter, Insup Lee 0001 |
Implementing a Real-Time Process Algebra in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Sara Kalvala |
HOL Around the World. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Thomas F. Melham |
A Package for Inductive Relation Definitions in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | X. Wang, Edward P. Stabler |
Formalization of VHDL Synthesis Procedure in Higher-Order Logic. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | David F. Martin, R. J. Toal |
Case Studies in Compiler Correctness Using HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | 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 |
DBLP BibTeX RDF |
|
| 1 | Sten Agerholm |
Mechanizing Program Verification in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Jim Grundy |
Window Inference in the HOL System. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Matt Kaufmann |
An Informal Discussion of Issues in Mechanically-Assisted Reasoning. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | J. W. Gambles, Phillip J. Windley |
An HOL Theory for Logic States with Indeterminate Strengths. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Paul Loewenstein |
Learning to use HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Sara Kalvala |
Developing an Interface for HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | William L. Harrison, Karl N. Levitt |
Mechanizing Security in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Flemming Andersen, Kim Dam Petersen |
Recursive Boolean Functions in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Phillip J. Windley |
The Practical Verification of Microprocessor Designs. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Joakim von Wright, Kaisa Sere |
Program Transformations and Refinements in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | R. D. Arthan |
A Report on ICL HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | George Fink, Myla Archer, Lie Yang |
PM: A Proof Manager for HOL and Other Provers. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Simon Bainbridge, Albert John Camilleri, Roger Fleming |
Industrial Application of Theorem Proving to System Level Design. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Malcolm C. Newey |
Proof Based Computation. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | W. Ploegaerts, Luc J. M. Claesen, Hugo De Man |
Defining Recursive Functions in HOL. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Rachel Cardell-Oliver |
On the use of the HOL system for Protocol Verification. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Ramayya Kumar, Thomas Kropf, Klaus Schneider 0001 |
Integrating a First-Order Automatic Prover in the HOL Environment. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | John M. Rushby |
Design Choices in Specification Languages and Verification Systems. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Kurt Keutzer |
The Need for Formal Verification in Hardware Design and What Formal Verification Has Not Done for Me Lately. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Shiu-Kai Chin |
Verifying Arithmetic Hardware in Higher-Order Logic. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license