Conferences in DBLP
Flemming Andersen , Kim Dam Petersen , Jimmi S. Pettersson Program Verification using HOL-UNITY. [Citation Graph (0, 0)][DBLP ] Conf ] Kim Dam Petersen Graph model of LAMBDA in Higher Order Logic. [Citation Graph (0, 0)][DBLP ] 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 ] Conf ] Don Syme Reasoning with the Formal Definition of Standard ML in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Myra Van Inwegen , Elsa L. Gunter HOL-ML. [Citation Graph (0, 0)][DBLP ] Conf ] Kees G. W. Goossens Stucture and Behaviour in Hardware Verification. [Citation Graph (0, 0)][DBLP ] 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 ] Conf ] Dirk Eisenbiegler , Klaus Schneider , Ramayya Kumar A Functional Approach for Formalizing Regular Hardware Structures. [Citation Graph (0, 0)][DBLP ] Conf ] Laurent Théry A Proof Development System for HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Rachel E. O. Roxas A HOL Package for Reasoning about Relations Defined by Mutual Induction. [Citation Graph (0, 0)][DBLP ] Conf ] Elsa L. Gunter A Broader Class of Trees for Recursive Type Definitions for HOL. [Citation Graph (0, 0)][DBLP ] Conf ] David Lorge Parnas Some Theorems We Should Prove. [Citation Graph (0, 0)][DBLP ] Conf ] John M. Rushby , Mandayam K. Srivas Using PVS to Prove Some Theorems Of David Parnas. [Citation Graph (0, 0)][DBLP ] 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 ] 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 ] Conf ] Juin-Yeu Lu , Shiu-Kai Chin Linking HOL to a VLSI CAD System. [Citation Graph (0, 0)][DBLP ] Conf ] Klaus Schneider , Ramayya Kumar , Thomas Kropf Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] Conf ] Anthony McIsaac A Formalization of Abstraction in LAMBDA. [Citation Graph (0, 0)][DBLP ] 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 ] 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 ] Conf ] David A. Fura , Phillip J. Windley , Arun K. Somani Abstraction Techniques for Modeling Real-World Interface Chips. [Citation Graph (0, 0)][DBLP ] Conf ] Sofiène Tahar , Ramayya Kumar Implementing a Methodology for Formally Verifying RISC Processors in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Sten Agerholm Domain Theory in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Ching-Tsun Chou Predicates, Temporal Logic, and Simulations. [Citation Graph (0, 0)][DBLP ] Conf ] I. S. W. B. Prasetya Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties. [Citation Graph (0, 0)][DBLP ] Conf ] Nancy A. Day , Jeffrey J. Joyce The Semantics of Statecharts in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Monica Nesi Value-Passing CCS in HOL. [Citation Graph (0, 0)][DBLP ] 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 ] Conf ] Wai Wong Modelling Bit Vectors in HOL: the word library. [Citation Graph (0, 0)][DBLP ] Conf ] Klaus Schneider , Ramayya Kumar , Thomas Kropf Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification. [Citation Graph (0, 0)][DBLP ] Conf ] Mark Aagaard , Miriam Leeser , Phillip J. Windley Toward a Super Duper Hardware Tactic. [Citation Graph (0, 0)][DBLP ] Conf ] Andrew D. Gordon A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. [Citation Graph (0, 0)][DBLP ] Conf ] John Harrison A HOL Decision Procedure for Elementary Real Algebra. [Citation Graph (0, 0)][DBLP ] Conf ] Konrad Slind AC Unification in HOL90. [Citation Graph (0, 0)][DBLP ] Conf ] Stephen H. Brackin , Shiu-Kai Chin Server-Process Restrictiveness in HOL. [Citation Graph (0, 0)][DBLP ] Conf ] Matthew J. Morley Safety in Railway Signalling Data: A Behavioural Analysis. [Citation Graph (0, 0)][DBLP ] Conf ] I. S. W. B. Prasetya On the Style of Mechanical Proving. [Citation Graph (0, 0)][DBLP ] 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 ] Conf ] Victor Carreño Verification in Higher Order Logic of Mutual Exclusion Algorithm. [Citation Graph (0, 0)][DBLP ] Conf ] Sara Kalvala Using Isabelle to Prove Simple Theorems. [Citation Graph (0, 0)][DBLP ] Conf ] 