Conferences in DBLP
Flemming Andersen , Kim Dam Petersen , Jimmi S. Pettersson Program Verification using HOL-UNITY. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:1-15 [Conf ] Kim Dam Petersen Graph model of LAMBDA in Higher Order Logic. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:16-28 [Conf ] Cui Zhang , Robert J. Shaw , Ronald A. Olsson , Karl N. Levitt , Myla Archer , Mark Heckman , Gregory D. Benson Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:29-42 [Conf ] Don Syme Reasoning with the Formal Definition of Standard ML in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:43-60 [Conf ] Myra Van Inwegen , Elsa L. Gunter HOL-ML. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:61-74 [Conf ] Kees G. W. Goossens Stucture and Behaviour in Hardware Verification. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:75-88 [Conf ] Catia M. Angelo , Luc J. M. Claesen , Hugo De Man Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:89-100 [Conf ] Dirk Eisenbiegler , Klaus Schneider , Ramayya Kumar A Functional Approach for Formalizing Regular Hardware Structures. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:101-114 [Conf ] Laurent Théry A Proof Development System for HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:115-128 [Conf ] Rachel E. O. Roxas A HOL Package for Reasoning about Relations Defined by Mutual Induction. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:129-140 [Conf ] Elsa L. Gunter A Broader Class of Trees for Recursive Type Definitions for HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:141-154 [Conf ] David Lorge Parnas Some Theorems We Should Prove. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:155-162 [Conf ] John M. Rushby , Mandayam K. Srivas Using PVS to Prove Some Theorems Of David Parnas. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:163-173 [Conf ] John Harrison , Laurent Théry Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:174-184 [Conf ] Jeffrey J. Joyce , Carl-Johan H. Seger The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:185-198 [Conf ] Juin-Yeu Lu , Shiu-Kai Chin Linking HOL to a VLSI CAD System. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:199-212 [Conf ] Klaus Schneider , Ramayya Kumar , Thomas Kropf Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:213-226 [Conf ] Anthony McIsaac A Formalization of Abstraction in LAMBDA. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:227-238 [Conf ] Tej Arora , Tony Leung , Karl N. Levitt , E. Thomas Schubert , Phillip J. Windley Report on the UCD Microcoded Viper Verification Project. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:239-252 [Conf ] Zheng Zhu , Jeffrey J. Joyce , Carl-Johan H. Seger Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:253-266 [Conf ] David A. Fura , Phillip J. Windley , Arun K. Somani Abstraction Techniques for Modeling Real-World Interface Chips. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:267-280 [Conf ] Sofiène Tahar , Ramayya Kumar Implementing a Methodology for Formally Verifying RISC Processors in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:281-294 [Conf ] Sten Agerholm Domain Theory in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:295-309 [Conf ] Ching-Tsun Chou Predicates, Temporal Logic, and Simulations. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:310-323 [Conf ] I. S. W. B. Prasetya Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:324-337 [Conf ] Nancy A. Day , Jeffrey J. Joyce The Semantics of Statecharts in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:338-351 [Conf ] Monica Nesi Value-Passing CCS in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:352-365 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:366-370 [Conf ] Wai Wong Modelling Bit Vectors in HOL: the word library. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:371-384 [Conf ] Klaus Schneider , Ramayya Kumar , Thomas Kropf Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:385-398 [Conf ] Mark Aagaard , Miriam Leeser , Phillip J. Windley Toward a Super Duper Hardware Tactic. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:399-412 [Conf ] Andrew D. Gordon A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:413-425 [Conf ] John Harrison A HOL Decision Procedure for Elementary Real Algebra. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:426-435 [Conf ] Konrad Slind AC Unification in HOL90. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:436-449 [Conf ] Stephen H. Brackin , Shiu-Kai Chin Server-Process Restrictiveness in HOL. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:450-463 [Conf ] Matthew J. Morley Safety in Railway Signalling Data: A Behavioural Analysis. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:464-474 [Conf ] I. S. W. B. Prasetya On the Style of Mechanical Proving. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:475-488 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:489-500 [Conf ] Victor Carreño Verification in Higher Order Logic of Mutual Exclusion Algorithm. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:501-513 [Conf ] Sara Kalvala Using Isabelle to Prove Simple Theorems. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:514-517 [Conf ]