Search results for "HUG"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Jeffrey J. Joyce, Carl-Johan H. Seger (eds.)	Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings	HUG	1994	DBLP DOI BibTeX RDF
1	Jeffrey J. Joyce, Carl-Johan H. Seger	The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover.	HUG	1993	DBLP DOI BibTeX RDF
1	Dirk Eisenbiegler, Klaus Schneider 0001, Ramayya Kumar	A Functional Approach for Formalizing Regular Hardware Structures.	HUG	1993	DBLP DOI BibTeX RDF
1	Ching-Tsun Chou	Predicates, Temporal Logic, and Simulations.	HUG	1993	DBLP DOI BibTeX RDF
1	Andrew D. Gordon 0001	A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion.	HUG	1993	DBLP DOI BibTeX RDF
1	Victor Carreño	Verification in Higher Order Logic of Mutual Exclusion Algorithm.	HUG	1993	DBLP DOI BibTeX RDF
1	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.	HUG	1993	DBLP DOI BibTeX RDF
1	Mark D. Aagaard, Miriam Leeser, Phillip J. Windley	Toward a Super Duper Hardware Tactic.	HUG	1993	DBLP DOI BibTeX RDF
1	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	DBLP DOI BibTeX RDF
1	David Lorge Parnas	Some Theorems We Should Prove.	HUG	1993	DBLP DOI BibTeX RDF
1	Elsa L. Gunter	A Broader Class of Trees for Recursive Type Definitions for HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	Myra Van Inwegen, Elsa L. Gunter	HOL-ML.	HUG	1993	DBLP DOI BibTeX RDF
1	Monica Nesi	Value-Passing CCS in HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	Laurent Théry	A Proof Development System for HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger	Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment.	HUG	1993	DBLP DOI BibTeX RDF
1	Kees G. W. Goossens	Stucture and Behaviour in Hardware Verification.	HUG	1993	DBLP DOI BibTeX RDF
1	Sara Kalvala	Using Isabelle to Prove Simple Theorems.	HUG	1993	DBLP DOI BibTeX RDF
1	Rachel E. O. Roxas	A HOL Package for Reasoning about Relations Defined by Mutual Induction.	HUG	1993	DBLP DOI BibTeX RDF
1	Don Syme	Reasoning with the Formal Definition of Standard ML in HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	Stephen H. Brackin, Shiu-Kai Chin	Server-Process Restrictiveness in HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	I. S. W. B. Prasetya	Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties.	HUG	1993	DBLP DOI BibTeX RDF
1	Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson	Program Verification using HOL-UNITY.	HUG	1993	DBLP DOI BibTeX RDF
1	Juin-Yeu Lu, Shiu-Kai Chin	Linking HOL to a VLSI CAD System.	HUG	1993	DBLP DOI BibTeX RDF
1	John M. Rushby, Mandayam K. Srivas	Using PVS to Prove Some Theorems Of David Parnas.	HUG	1993	DBLP DOI BibTeX RDF
1	Nancy A. Day, Jeffrey J. Joyce	The Semantics of Statecharts in HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	I. S. W. B. Prasetya	On the Style of Mechanical Proving.	HUG	1993	DBLP DOI BibTeX RDF
1	Tej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley	Report on the UCD Microcoded Viper Verification Project.	HUG	1993	DBLP DOI BibTeX RDF
1	John Harrison 0001	A HOL Decision Procedure for Elementary Real Algebra.	HUG	1993	DBLP DOI BibTeX RDF
1	Matthew J. Morley	Safety in Railway Signalling Data: A Behavioural Analysis.	HUG	1993	DBLP DOI BibTeX RDF	application specific languages, Safety-critical systems, higher-order logic, railway signalling
1	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.	HUG	1993	DBLP DOI BibTeX RDF
1	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	DBLP DOI BibTeX RDF
1	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	DBLP DOI BibTeX RDF
1	Anthony McIsaac	A Formalization of Abstraction in LAMBDA.	HUG	1993	DBLP DOI BibTeX RDF
1	David A. Fura, Phillip J. Windley, Arun K. Somani	Abstraction Techniques for Modeling Real-World Interface Chips.	HUG	1993	DBLP DOI BibTeX RDF
1	Kim Dam Petersen	Graph model of LAMBDA in Higher Order Logic.	HUG	1993	DBLP DOI BibTeX RDF
1	Catia M. Angelo, Luc J. M. Claesen, Hugo De Man	Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	Sten Agerholm	Domain Theory in HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	Konrad Slind	AC Unification in HOL90.	HUG	1993	DBLP DOI BibTeX RDF
1	Wai Wong	Modelling Bit Vectors in HOL: the word library.	HUG	1993	DBLP DOI BibTeX RDF
1	Sofiène Tahar, Ramayya Kumar	Implementing a Methodology for Formally Verifying RISC Processors in HOL.	HUG	1993	DBLP DOI BibTeX RDF
1	John Harrison 0001, Laurent Théry	Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.	HUG	1993	DBLP DOI BibTeX RDF

Publications at "HUG"( http://dblp.L3S.de/Venues/HUG )