Search results for "HOL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
16	Hamdi Yahyaoui, Mourad Debbabi, Nadia Tawbi	A Denotational Semantic Model for Validating JVML/CLDC Optimizations under Isabelle/HOL.	QSIC	2007	DBLP DOI BibTeX RDF
16	Juliano Manabu Iyoda	Translating HOL functions to hardware.		2007	RDF
16	Cheng Wang, Ross D. Murch	Optimal downlink multi-user MIMO cross-layer scheduling using HOL packet waiting time.	IEEE Trans. Wirel. Commun.	2006	DBLP DOI BibTeX RDF
16	Rabeb Mizouni, Sofiène Tahar, Paul Curzon	Hybrid verification integrating HOL theorem proving with MDG model checking.	Microelectron. J.	2006	DBLP DOI BibTeX RDF
16	Tom Ridge	Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL	CoRR	2006	DBLP BibTeX RDF
16	J. Nathan Foster, Dimitrios Vytiniotis	A Theory of Featherweight Java in Isabelle/HOL.	Arch. Formal Proofs	2006	DBLP BibTeX RDF
16	Norbert Schirmer	Verification of sequential imperative programs in Isabelle-HOL.		2006	RDF
16	Sean McLaughlin, Clark W. Barrett, Yeting Ge	Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.	PDPAR@CAV	2005	DBLP DOI BibTeX RDF
16	Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen Mülling	Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL.	COCV@ETAPS	2005	DBLP DOI BibTeX RDF
16	Joe Hurd, Annabelle McIver, Carroll Morgan	Probabilistic guarded commands mechanized in HOL.	Theor. Comput. Sci.	2005	DBLP DOI BibTeX RDF
16	Joris Walraevens, Bart Steyaert, Marc Moeneclaey, Herwig Bruneel	Delay Analysis of a HOL Priority Queue.	Telecommun. Syst.	2005	DBLP DOI BibTeX RDF	discrete-time priority queue, multimedia
16	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	Mathematics, Algorithms, Proofs	2005	DBLP BibTeX RDF
16	Joris Walraevens, Bart Steyaert, Marc Moeneclaey, Herwig Bruneel	A Discrete-Time HOL Priority Queue with Multiple Traffic Classes.	ICN (1)	2005	DBLP DOI BibTeX RDF
16	Anthony C. J. Fox	An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL.	CALCO	2005	DBLP DOI BibTeX RDF
16	Sergey Tverdyshev	Combination of Isabelle/HOL with Automatic Tools.	FroCoS	2005	DBLP DOI BibTeX RDF
16	Daniel Hausmann 0001, Till Mossakowski, Lutz Schröder	Iterative Circular Coinduction for CoCasl in Isabelle/HOL.	FASE	2005	DBLP DOI BibTeX RDF
16	Joe Hurd, Annabelle McIver, Carroll Morgan	Probabilistic Guarded Commands Mechanized in HOL.	QAPL	2004	DBLP DOI BibTeX RDF
16	Tjark Weber	Bounded Model Generation for Isabelle/HOL.	D/PDPAR@IJCAR	2004	DBLP DOI BibTeX RDF
16	Norbert Schirmer	Analysing the Java package/access concepts in Isabelle/HOL.	Concurr. Pract. Exp.	2004	DBLP DOI BibTeX RDF
16	Jonathan P. Seldin	Interpreting HOL in the calculus of constructions.	J. Appl. Log.	2004	DBLP DOI BibTeX RDF
16	Orieta Celiku, Annabelle McIver	Cost-Based Analysis of Probabilistic Programs Mechanised in HOL.	Nord. J. Comput.	2004	DBLP BibTeX RDF
16	John Longley, Randy Pollack	Reasoning About CBV Functional Programs in Isabelle/HOL.	TPHOLs	2004	DBLP DOI BibTeX RDF
16	Jan Olaf Blech, Sabine Glesner	A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL.	GI Jahrestagung (2)	2004	DBLP BibTeX RDF
16	Kenro Yatake, Toshiaki Aoki, Takuya Katayama	Collaboration-based verification of Object-Oriented models in HOL.	VVEIS	2004	DBLP BibTeX RDF
16	Stefan Berghofer, Tobias Nipkow	Random Testing in Isabelle/HOL.	SEFM	2004	DBLP DOI BibTeX RDF
16	Nicole Rauch, Burkhart Wolff	Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL.	FMICS	2003	DBLP DOI BibTeX RDF
16	Achim D. Brucker, Frank Rittinger, Burkhart Wolff	HOL-Z 2.0: A Proof Environment for Z-Specifications.	J. Univers. Comput. Sci.	2003	DBLP DOI BibTeX RDF
16	Christine Röckl, Daniel Hirschkoff	A fully adequate shallow embedding of the [pi]-calculus in Isabelle/HOL with mechanized syntax analysis.	J. Funct. Program.	2003	DBLP DOI BibTeX RDF
16	Thumrongsak Kosiyatrakul, Susan Older, Polar Humenn, Shiu-Kai Chin	Implementing a Calculus for Distributed Access Control in Higher Order Logic and HOL.	MMM-ACNS	2003	DBLP DOI BibTeX RDF
16	Haykal Tej	HOL-CSP: mechanised formal devlopment mof concurrent processes.		2003	RDF
16	Sylvain Delas, Ravi Mazumdar, Catherine Rosenberg	Tail Asymptotics for HOL Priority Queues Handling a Large Number of Independent Stationary Sources.	Queueing Syst. Theory Appl.	2002	DBLP DOI BibTeX RDF
16	Michael Norrish, Konrad Slind	A Thread of HOL Development.	Comput. J.	2002	DBLP DOI BibTeX RDF
16	Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel 0001	Isabelle/HOL - A Proof Assistant for Higher-Order Logic		2002	DOI RDF
16	Achim D. Brucker, Burkhart Wolff	HOL-OCL: Experiences, Consequences and Design Choices.	UML	2002	DBLP DOI BibTeX RDF	refinement, OCL, formal semantics, constraint languages
16	Achim D. Brucker, Burkhart Wolff	A Proposal for a Formal OCL Semantics in Isabelle/HOL.	TPHOLs	2002	DBLP DOI BibTeX RDF	shallow embedding, UML, testing, OCL, Isabelle
16	Tobias Nipkow	Structured Proofs in Isar/HOL.	TYPES	2002	DBLP DOI BibTeX RDF
16	Leonor Prensa Nieto	Verification of parallel programs with the Owicki-Gries and Rely-Guarantee methods in Isabelle, HOL.		2002	RDF
16	Haiyan Xiong	Providing a formal linkage between MDG and HOL based on a verified MDG system.		2002	RDF
16	David von Oheimb	Hoare logic for Java in Isabelle/HOL.	Concurr. Comput. Pract. Exp.	2001	DBLP DOI BibTeX RDF
16	Gilles Dowek, Thérèse Hardin, Claude Kirchner	HOL-λσ: an intentional first-order expression of higher-order logic.	Math. Struct. Comput. Sci.	2001	DBLP BibTeX RDF
16	Christine Röckl	A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations.	MERLIN	2001	DBLP DOI BibTeX RDF
16	Yasuhiko Minamide, Koji Okuma	Verifying the CPS Transformation in Isabelle/HOL.	APLAS	2001	DBLP BibTeX RDF
16	David von Oheimb	Analyzing Java in Isabelle-HOL: formalization, type safety and Hoare logic. (PDF / PS)		2001	RDF
16	John Harrison 0001	Floating Point Verification in HOL Light: The Exponential Function.	Formal Methods Syst. Des.	2000	DBLP DOI BibTeX RDF
16	Mike Gordon	From LCF to HOL: a short history.	Proof, Language, and Interaction	2000	DBLP BibTeX RDF
16	Christine Röckl	Proving Write Invalidate Cache Coherence with Bisimulations in Isabelle/HOL.	FBT	2000	DBLP BibTeX RDF
16	Wai Wong	Validation of HOL Proofs by Proof Checking.	Formal Methods Syst. Des.	1999	DBLP DOI BibTeX RDF
16	Sofiène Tahar, Paul Curzon	Comparing HOL and MDG: a Case Study on the Verification of an ATM Switch Fabric.	Nord. J. Comput.	1999	DBLP BibTeX RDF
16	Wolfgang Naraschewski, Tobias Nipkow	Type Inference Verified: Algorithm W in Isabelle/HOL.	J. Autom. Reason.	1999	DBLP DOI BibTeX RDF
16	Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch	HOLCF=HOL+LCF.	J. Funct. Program.	1999	DBLP DOI BibTeX RDF
16	Stefan Berghofer, Markus Wenzel 0001	Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.	TPHOLs	1999	DBLP DOI BibTeX RDF
16	Gilles Dowek, Thérèse Hardin, Claude Kirchner	HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic.	RTA	1999	DBLP DOI BibTeX RDF
16	Tobias Nipkow, Leonor Prensa Nieto	Owicki/Gries in Isabelle/HOL.	FASE	1999	DBLP DOI BibTeX RDF
16	Michael Norrish	C formalised in HOL		1999	RDF
16	John Harrison 0001, Laurent Théry	A Skeptic's Approach to Combining HOL and Maple.	J. Autom. Reason.	1998	DBLP DOI BibTeX RDF
16	Norbert Völker	Ein Rahmen zur Verifikation von SPS-Funktionsbausteinen in HOL.		1998	RDF
16	W. O. David Griffioen, Marieke Huisman	A Comparison of PVS and Isabelle/HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
16	Demetres D. Kouvatsos, Irfan-Ullah Awan	Approximate Analysis of Arbitrary Open Networks with HOL Priorities and PBS Scheme.	ESM	1998	DBLP BibTeX RDF
16	Thomas Santen	On the Semantic Relation of Z and HOL.	ZUM	1998	DBLP DOI BibTeX RDF
16	Christoph Lüth, Einar W. Karlsen, Kolyang 0001, Stefan Westmeier, Burkhart Wolff	HOL-Z in the UniForM-Wokbench - A Case Study in Tool Integration for Z.	ZUM	1998	DBLP DOI BibTeX RDF
16	David A. Basin, Stefan Friedrich 0001	Combining WS1S and HOL.	FroCoS	1998	DBLP BibTeX RDF
16	Jim Grundy, Thomas Långbacka	Recording HOL Proofs in a Structured Browsable Format.	AMAST	1997	DBLP DOI BibTeX RDF
16	John Harrison 0001	Floating Point Verification in HOL Light: The Exponential Function.	AMAST	1997	DBLP DOI BibTeX RDF
16	Matthias Mutz	Automatic post-synthesis verification support for a high level synthesis step by using the HOL theorem proving system.	CHARME	1997	DBLP BibTeX RDF
16	Monica Nesi	Mechanising a modal logic for value-passing agents in HOL.	INFINITY	1996	DBLP DOI BibTeX RDF
16	Vincent Zammit	A Mechanisation of Computability Theory in HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	John Harrison 0001	Stålmarck's Algorithm as a HOL Derived Rule.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar	Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Stephen H. Brackin	Deciding Cryptographic Protocol Adequacy with HOL: The Implementation.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	John Harrison 0001	A Mizar Mode for HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Sofiène Tahar, Paul Curzon	A Comparison of MDG and HOL for Hardware Verification.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Sten Agerholm, Ilya Beylin, Peter Dybjer	A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Douglas J. Howe	Importing Mathematics from HOL into Nuprl.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Kolyang 0001, Thomas Santen, Burkhart Wolff	A Structure Preserving Encoding of Z in Isabelle/HOL.	TPHOLs	1996	DBLP DOI BibTeX RDF
16	Douglas J. Howe	Semantic Foundations for Embedding HOL in Nuprl.	AMAST	1996	DBLP DOI BibTeX RDF
16	Wolfgang Naraschewski, Tobias Nipkow	Type Inference Verified: Algorithm W in Isabelle/HOL.	TYPES	1996	DBLP DOI BibTeX RDF
16	M. Vishnu, Jon W. Mark	HOL-EDD: A Flexible Service Scheduling Scheme for ATM Networks.	INFOCOM	1996	DBLP DOI BibTeX RDF
16	John Harrison 0001	HOL Light: A Tutorial Introduction.	FMCAD	1996	DBLP DOI BibTeX RDF
16	Ralf Reetz, Thomas Kropf	A Flowgraph Semantics of VHDL: Toward a VHDL Verification Workbench in HOL.	Formal Methods Syst. Des.	1995	DBLP DOI BibTeX RDF
16	Jonathan P. Bowen, Mike Gordon	A shallow embedding of Z in HOL.	Inf. Softw. Technol.	1995	DBLP DOI BibTeX RDF
16	John Harrison 0001	Binary Decision Diagrams as a HOL Derived Rule.	Comput. J.	1995	DBLP DOI BibTeX RDF
16	Elsa L. Gunter, Savi Maharaj	Studying the ML Module System in HOL.	Comput. J.	1995	DBLP DOI BibTeX RDF
16	Sten Agerholm	LCF Examples in HOL.	Comput. J.	1995	DBLP DOI BibTeX RDF
16	Joakim von Wright	Representing Higher-Order Logic Proofs in HOL.	Comput. J.	1995	DBLP DOI BibTeX RDF
16	Rachel Cardell-Oliver	HTTDs and HOL.	Formal Development of Reactive Systems	1995	DBLP DOI BibTeX RDF
16	Rix Groenboom, Chris Hendriks, Indra Polak, Jan Terlouw, Jan Tijmen Udding	Algebraic Proof Assistants in HOL.	MPC	1995	DBLP DOI BibTeX RDF
16	Catia M. Angelo, Luc J. M. Claesen, Hugo De Man	Modeling Multi-rate DSP Specification Semantics for Formal Transformational Design in HOL.	Formal Methods Syst. Des.	1994	DBLP DOI BibTeX RDF
16	John Harrison 0001	Constructing the Real Numbers in HOL.	Formal Methods Syst. Des.	1994	DBLP DOI BibTeX RDF
16	Thomas F. Melham	A Mechanized Theory of the Pi-Calculus in HOL.	Nord. J. Comput.	1994	DBLP BibTeX RDF
16	Graham Hutton	Book Review: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic by Mike Gordon and Tom Melham (eds.), Cambridge University Press, 1993, ISBN 0-521-44189-7.	J. Funct. Program.	1994	DBLP DOI BibTeX RDF
16	Thomas Forster	Weak Systems of Set Theory Related to HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
16	Jean-Paul Bodeveix, Mamoun Filali, P. Roche	Towards a HOL Theory and Memory.	TPHOLs	1994	DBLP DOI BibTeX RDF
16	Tobias Nipkow, Konrad Slind	I/Q Automata in Isabelle/HOL.	TYPES	1994	DBLP DOI BibTeX RDF
16	Jonathan P. Bowen, Michael J. C. Gordon	Z and HOL.	Z User Workshop	1994	DBLP DOI BibTeX RDF
16	Franz Regensburger	HOLCF: eine konservative Erweiterung von HOL um LCF.		1994	RDF
16	Catia M. Angelo, Diederik Verkest, Luc J. M. Claesen, Hugo De Man	On the Comparison of HOL and Boyer-Moore for Formal Hardware Verification.	Formal Methods Syst. Des.	1993	DBLP DOI BibTeX RDF
16	Roger Hale, Rachel Cardell-Oliver, John Herbert	An Embedding of Timed Transition Systems in HOL.	Formal Methods Syst. Des.	1993	DBLP DOI BibTeX RDF
16	Thomas F. Melham	The HOL Logic Extended with Quantification over Type Variables.	Formal Methods Syst. Des.	1993	DBLP DOI BibTeX RDF
16	John Harrison 0001, Laurent Théry	Reasoning About the Reals: The Marriage of HOL and Maple.	LPAR	1993	DBLP DOI BibTeX RDF
16	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