HUG

Keyphrases

Publications

volume 780, 1994

Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings HUG 780 (1994)

1993

Jeffrey J. Joyce, Carl-Johan H. Seger
The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. HUG (1993)
Dirk Eisenbiegler, Klaus Schneider, Ramayya Kumar
A Functional Approach for Formalizing Regular Hardware Structures. HUG (1993)
Ching-Tsun Chou
Predicates, Temporal Logic, and Simulations. HUG (1993)
Andrew D. Gordon
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. HUG (1993)
Victor Carreño
Verification in Higher Order Logic of Mutual Exclusion Algorithm. HUG (1993)
Klaus Schneider, Ramayya Kumar, Thomas Kropf
Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic. HUG (1993)
Mark D. Aagaard, Miriam Leeser, Phillip J. Windley
Toward a Super Duper Hardware Tactic. HUG (1993)
Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger
From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation. HUG (1993)
David Lorge Parnas
Some Theorems We Should Prove. HUG (1993)
Elsa L. Gunter
A Broader Class of Trees for Recursive Type Definitions for HOL. HUG (1993)
Myra Van Inwegen, Elsa L. Gunter
HOL-ML. HUG (1993)
Monica Nesi
Value-Passing CCS in HOL. HUG (1993)
Laurent Théry
A Proof Development System for HOL. HUG (1993)
Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger
Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment. HUG (1993)
Kees G. W. Goossens
Stucture and Behaviour in Hardware Verification. HUG (1993)
Sara Kalvala
Using Isabelle to Prove Simple Theorems. HUG (1993)
Rachel E. O. Roxas
A HOL Package for Reasoning about Relations Defined by Mutual Induction. HUG (1993)
Don Syme
Reasoning with the Formal Definition of Standard ML in HOL. HUG (1993)
Stephen H. Brackin, Shiu-Kai Chin
Server-Process Restrictiveness in HOL. HUG (1993)
I. S. W. B. Prasetya
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties. HUG (1993)
Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson
Program Verification using HOL-UNITY. HUG (1993)
Juin-Yeu Lu, Shiu-Kai Chin
Linking HOL to a VLSI CAD System. HUG (1993)
John M. Rushby, Mandayam K. Srivas
Using PVS to Prove Some Theorems Of David Parnas. HUG (1993)
Nancy A. Day, Jeffrey J. Joyce
The Semantics of Statecharts in HOL. HUG (1993)
I. S. W. B. Prasetya
On the Style of Mechanical Proving. HUG (1993)
Tej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley
Report on the UCD Microcoded Viper Verification Project. HUG (1993)
John Harrison
A HOL Decision Procedure for Elementary Real Algebra. HUG (1993)
Matthew J. Morley
Safety in Railway Signalling Data: A Behavioural Analysis. HUG (1993)
Klaus Schneider, Ramayya Kumar, Thomas Kropf
Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification. HUG (1993)
Cui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark R. Heckman, Gregory D. Benson
Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL. HUG (1993)
Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. HUG (1993)
Anthony McIsaac
A Formalization of Abstraction in LAMBDA. HUG (1993)
David A. Fura, Phillip J. Windley, Arun K. Somani
Abstraction Techniques for Modeling Real-World Interface Chips. HUG (1993)
Kim Dam Petersen
Graph model of LAMBDA in Higher Order Logic. HUG (1993)
Catia M. Angelo, Luc J. M. Claesen, Hugo De Man
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL. HUG (1993)
Sten Agerholm
Domain Theory in HOL. HUG (1993)
Konrad Slind
AC Unification in HOL90. HUG (1993)
Wai Wong
Modelling Bit Vectors in HOL: the word library. HUG (1993)
Sofiène Tahar, Ramayya Kumar
Implementing a Methodology for Formally Verifying RISC Processors in HOL. HUG (1993)
John Harrison, Laurent Théry
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. HUG (1993)