Search results for "HOL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
117	Steven Obua, Sebastian Skalberg	Importing HOL into Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF
86	Cheng-Shang Chang, Duan-Shin Lee, Chao-Lin Yu	Generalization of the Pollaczek-Khinchin formula for throughput analysis of input-buffered switches.	INFOCOM	2005	DBLP DOI BibTeX RDF
83	Osman Hasan, Sofiène Tahar	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Real-time systems, Communication protocols, Higher-order-logic, Probability theory, HOL theorem prover
73	Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford	Formally Linking MDG and HOL Based on a Verified MDG System.	IFM	2002	DBLP DOI BibTeX RDF	hybrid verification systems, deductive theorem proving, symbolic state enumeration, usability verification, hardware verification
73	Norbert Völker	Disjoint Sums over Type Classes in HOL.	TPHOLs	1999	DBLP DOI BibTeX RDF
73	Juin-Yeu Lu, Shiu-Kai Chin	Linking HOL to a VLSI CAD System.	HUG	1993	DBLP DOI BibTeX RDF
69	Sean McLaughlin	An Interpretation of Isabelle/HOL in HOL Light.	IJCAR	2006	DBLP DOI BibTeX RDF
65	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	Reachability analysis using multiway decision graphs in the HOL theorem prover.	SAC	2008	DBLP DOI BibTeX RDF	reachability analysis, HOL, multiway decision graphs
64	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs.	J. Comput. Sci. Technol.	2009	DBLP DOI BibTeX RDF	correctness, reachability analysis, multiway decision graphs, HOL theorem prover
64	Achim D. Brucker, Burkhart Wolff	Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing.	TAP	2007	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation
63	John Harrison 0001	HOL Light: An Overview.	TPHOLs	2009	DBLP DOI BibTeX RDF
63	Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann	An Integration of HOL and ACL2.	FMCAD	2006	DBLP DOI BibTeX RDF
63	Tarek Mhamdi, Sofiène Tahar	Providing Automated Verification in HOL Using MDGs.	ATVA	2004	DBLP DOI BibTeX RDF
63	Behzad Akbarpour, Sofiène Tahar	A Methodology for the Formal Verification of FFT Algorithms in HOL.	FMCAD	2004	DBLP DOI BibTeX RDF
63	Klaus Schneider 0001, Dirk W. Hoffmann	A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.	TPHOLs	1999	DBLP DOI BibTeX RDF
63	Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy	System Description: An Interface Between CLAM and HOL.	CADE	1998	DBLP DOI BibTeX RDF
63	Brian T. Graham	An Interpretation of NODEN in HOL.	TPHOLs	1994	DBLP DOI BibTeX RDF
59	Morten P. Lindegaard, Anne E. Haxthausen	Proof Support for RAISE by a Reuse Approach Based on Institutions.	AMAST	2004	DBLP DOI BibTeX RDF	proof support, Institutions, algebraic semantics, HOL, RSL
55	Osman Hasan, Sofiène Tahar	Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function.	IFM	2007	DBLP DOI BibTeX RDF	Higher-Order-Logic, Interactive Theorem Proving, HOL, Probabilistic Systems, Cumulative Distribution Function
55	Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith 0008, Keith Wansbrough	Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations.	POPL	2006	DBLP DOI BibTeX RDF	specification, TCP/IP, network protocols, operational semantics, API, conformance testing, higher-order logic, sockets, HOL
54	Anduo Wang, Fei He 0001, Ming Gu 0001, Xiaoyu Song	Verifying Java Programs By Theorem Prover HOL.	COMPSAC (1)	2006	DBLP DOI BibTeX RDF
54	John Harrison 0001	Towards Self-verification of HOL Light.	IJCAR	2006	DBLP DOI BibTeX RDF
54	Teresa Nachiondo Frinós, José Flich, José Duato	Destination-Based HoL Blocking Elimination.	ICPADS (1)	2006	DBLP DOI BibTeX RDF
54	Thomas Tuerk, Klaus Schneider 0001, Mike Gordon	Model Checking PSL Using HOL and SMV.	Haifa Verification Conference	2006	DBLP DOI BibTeX RDF
54	John Harrison 0001	A HOL Theory of Euclidean Space.	TPHOLs	2005	DBLP DOI BibTeX RDF
54	Joe Hurd	Integrating Gandalf and HOL.	TPHOLs	1999	DBLP DOI BibTeX RDF
54	Hajime Sawamura, Daisaku Asanuma	Mechanizing Relevant Logics with HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
48	Osman Hasan, Sofiène Tahar	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coupon collector’s problem, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties, HOL theorem prover
48	Matt Fairtlough, Michael Mendler, Xiaochun Cheng	Abstraction and Refinement in Higher Order Logic.	TPHOLs	2001	DBLP DOI BibTeX RDF
48	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
46	Sander Vermolen, Jozef Hooman, Peter Gorm Larsen	Proving consistency of VDM models using HOL.	SAC	2010	DBLP DOI BibTeX RDF	verification, theorem proving, VDM, HOL, model consistency
46	Achim D. Brucker, Burkhart Wolff	An Extensible Encoding of Object-oriented Data Models in hol.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Verification, Theorem proving, Object-oriented data models, hol
46	Behzad Akbarpour, Abdelkader Dekdouk, Sofiène Tahar	Formalization of Cadence SPW Fixed-Point Arithmetic in HOL.	IFM	2002	DBLP DOI BibTeX RDF	SPW, Theorem-Proving, Signal Processing, Floating-point, Fixed-point, HOL
45	Markus Kaiser 0002, Ralf Lämmel	An Isabelle/HOL-based model of stratego-like traversal strategies.	PPDP	2009	DBLP DOI BibTeX RDF	generic functional programming, traversal strategies, domain specific languages, rewriting, isabelle/hol, software transformation, stratego
45	Stephen H. Brackin	A HOL extension of GNY for automatically analyzing cryptographic protocols.	CSFW	1996	DBLP DOI BibTeX RDF	HOL extension, automatically analyzing cryptographic protocols, higher order logic theory, authentication properties, protocol properties, hash operations, key-exchange algorithms, formal specification, cryptography, message authentication, access protocols, message authentication codes, multiple encryption, belief maintenance, belief logic
45	B. M. Subraya, Anshul Kumar, Shashi Kumar	An HOL based framework for design of correct high level synthesizers.	VLSI Design	1995	DBLP DOI BibTeX RDF	HOL based framework, high level synthesizer design, design correctness guarantee, verifiable templates, synthesis module correctness, formal verification, high level synthesis, modularity, formal logic, higher order logic, verification process, formal framework
44	Peter V. Homeier	The HOL-Omega Logic.	TPHOLs	2009	DBLP DOI BibTeX RDF
44	Alexander Schimpf, Stephan Merz, Jan-Georg Smaus	Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
44	Achim D. Brucker, Burkhart Wolff	hol-TestGen.	FASE	2009	DBLP DOI BibTeX RDF	symbolic test-case generations, theorem proving, black box testing, white box testing, interactive testing
44	Osman Hasan, Sofiène Tahar	Verification of Expectation Properties for Discrete Random Variables in HOL.	TPHOLs	2007	DBLP DOI BibTeX RDF
44	Robert L. Constable, Wojciech Moczydlowski	Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics.	IJCAR	2006	DBLP DOI BibTeX RDF
44	Teresa Nachiondo Frinós, José Flich, José Duato	Efficient Reduction of HOL Blocking in Multistage Networks.	IPDPS	2005	DBLP DOI BibTeX RDF
44	Achim D. Brucker, Burkhart Wolff	Interactive Testing with HOL-TestGen.	FATES	2005	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, black box testing, white box testing, interactive testing
44	Florian Kammüller, Jeff W. Sanders	Idempotent Relations in Isabelle/HOL.	ICTAC	2004	DBLP DOI BibTeX RDF
44	Joe Hurd	An LCF-Style Interface between HOL and First-Order Logic.	CADE	2002	DBLP DOI BibTeX RDF
44	Graeme Smith 0001, Florian Kammüller, Thomas Santen	Encoding Object-Z in Isabelle/HOL.	ZB	2002	DBLP DOI BibTeX RDF	reference semantics, Object-Z, higher-order logic, Isabelle
44	Freek Wiedijk	Mizar Light for HOL Light.	TPHOLs	2001	DBLP DOI BibTeX RDF
44	Pavel Naumov, Mark-Oliver Stehr, José Meseguer 0001	The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability).	TPHOLs	2001	DBLP DOI BibTeX RDF
44	Koichi Takahashi, Masami Hagiya	Proving as Editing HOL Tactics.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Tactic-Based Theorem Prover, User interface, Higher Order Logic, Emacs
44	Haiyan Xiong, Paul Curzon, Sofiène Tahar	Importing MDG Verification Results into HOL.	TPHOLs	1999	DBLP DOI BibTeX RDF
44	Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon	An Interface between Clam and HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
44	Thomas Santen	A Theory of Structured Model-Based Specifications in Isabelle/HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
44	John Harrison 0001	Verifying the Accuracy of Polynomial Approximations in HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
44	Don Syme	A New Interface for HOL - Ideas, Issues and Implementation.	TPHOLs	1995	DBLP DOI BibTeX RDF
44	Otmane Aït Mohamed	Mechanizing a pi-Calculus Equivalence in HOL.	TPHOLs	1995	DBLP DOI BibTeX RDF
44	Flemming Andersen, Ulla Binau, Karsten Nyblad, Kim Dam Petersen, Jimmi S. Pettersson	The HOL-UNITY Verification System.	TAPSOFT	1995	DBLP DOI BibTeX RDF
44	Elsa L. Gunter	A Broader Class of Trees for Recursive Type Definitions for HOL.	HUG	1993	DBLP DOI BibTeX RDF
44	Myra Van Inwegen, Elsa L. Gunter	HOL-ML.	HUG	1993	DBLP DOI BibTeX RDF
44	Monica Nesi	Value-Passing CCS in HOL.	HUG	1993	DBLP DOI BibTeX RDF
44	Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson	Program Verification using HOL-UNITY.	HUG	1993	DBLP DOI BibTeX RDF
39	Deng Pan, Yuanyuan Yang 0001	FIFO-Based Multicast Scheduling Algorithm for Virtual Output Queued Packet Switches.	IEEE Trans. Computers	2005	DBLP DOI BibTeX RDF	virtual output queued (VOQ) switch, head of line (HOL) blocking, scheduling, Multicast, crossbar switch, multicast switch
39	Sabine Glesner, Jan Olaf Blech	Coalgebraic Semantics for Component Systems.	Architecting Systems with Trustworthy Components	2004	DBLP DOI BibTeX RDF	verification, semantics, Components, Isabelle/HOL, coinduction, component interaction
39	David von Oheimb, Tobias Nipkow	Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited.	FME	2002	DBLP DOI BibTeX RDF	Java, Hoare logic, side effects, dynamic binding, Isabelle/HOL, auxiliary variables
39	David von Oheimb	Hoare Logic for Mutual Recursion and Local Variables.	FSTTCS	1999	DBLP DOI BibTeX RDF	axiomaticsemantics, relative completeness, local variables, call-by-value parameters, soundness, Hoare logic, Isabelle/HOL, mutual recursion
38	Behzad Akbarpour, Sofiène Tahar	An approach for the formal verification of DSP designs using Theorem proving.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2006	DBLP DOI BibTeX RDF
38	Herman Geuvers	(In)consistency of Extensions of Higher Order Logic and Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
38	John Harrison 0001	Formalizing Basic First Order Model Theory.	TPHOLs	1998	DBLP DOI BibTeX RDF
38	Wolfgang Naraschewski, Markus Wenzel 0001	Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic.	TPHOLs	1998	DBLP DOI BibTeX RDF
38	Michael Jurczyk	Performance and Implementation Aspects of Higher Order Head-of-Line Blocking Switch Boxes.	ICPP	1997	DBLP DOI BibTeX RDF	central memory buffering, higher order blocking effects, multistage cube network, nonuniform traffic patterns, switch box implementation
38	Ralf Reetz	Deep Embedding VHDL.	TPHOLs	1995	DBLP DOI BibTeX RDF
36	Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds	An embedding of the ACL2 logic in HOL.	ACL2	2006	DBLP DOI BibTeX RDF	HOL4, proof oracle, sound translation, verification, formal methods, logic, first-order logic, higher-order logic, ACL2, HOL
36	Behzad Akbarpour, Sofiène Tahar, Abdelkader Dekdouk	Formalization of Fixed-Point Arithmetic in HOL.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	theorem-proving, floating-point arithmetic, fixed-point arithmetic, HOL
35	Sa'ed Abed, Otmane Aït Mohamed	MDGs Reduction Technique Based on the HOL Theorem Prover.	ISMVL	2010	DBLP DOI BibTeX RDF	Soundness, Reduction Techniques, Multiway Decision Graphs, HOL Theorem Prover
35	Christian Urban	Nominal Techniques in Isabelle/HOL.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Nominal logic work, Lambda-calculus, Theorem provers
35	Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff	HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier.	TPHOLs	2008	DBLP DOI BibTeX RDF
35	Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford	Providing a formal linkage between MDG and HOL.	Formal Methods Syst. Des.	2007	DBLP DOI BibTeX RDF	Verification system correctness, Hybrid verification systems, Formal hardware verification, Usability verification
35	Eunsuk Kang, Mark D. Aagaard	Improving the Usability of HOL Through Controlled Automation Tactics.	TPHOLs	2007	DBLP DOI BibTeX RDF
35	James Reynolds	Automatically Translating Type and Function Definitions from HOL to ACL2.	TPHOLs	2007	DBLP DOI BibTeX RDF
35	Carsten Schürmann, Mark-Oliver Stehr	An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf.	LPAR	2006	DBLP DOI BibTeX RDF
35	Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell	Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL.	ICNP	2006	DBLP DOI BibTeX RDF
35	Abu Nasser Mohammed Abdullah, Behzad Akbarpour, Sofiène Tahar	Formal Analysis and Verification of an OFDM Modem Design using HOL.	FMCAD	2006	DBLP DOI BibTeX RDF
35	David A. Basin, Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff	Verification of a Signature Architecture with HOL-Z.	FM	2005	DBLP DOI BibTeX RDF
35	Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner	Formal Verification of Dead Code Elimination in Isabelle/HOL.	SEFM	2005	DBLP DOI BibTeX RDF
35	José Duato, José Flich, Teresa Nachiondo Frinós	A Cost-Effective Technique to Reduce HOL Blocking in Single-Stage and Multistage Switch Fabrics.	PDP	2004	DBLP DOI BibTeX RDF
35	Stefan Berghofer	Extracting a Normalization Algorithm in Isabelle/HOL.	TYPES	2004	DBLP DOI BibTeX RDF
35	Behzad Akbarpour, Sofiène Tahar	Modeling System C Fixed-Point Arithmetic in HOL.	ICFEM	2003	DBLP DOI BibTeX RDF
35	María Engracia Gómez, José Flich, Antonio Robles, Pedro López 0001, José Duato	VOQSW: A Methodology to Reduce HOL Blocking in InfiniBand Networks.	IPDPS	2003	DBLP DOI BibTeX RDF	InfiniBand network, virtual lanes, irregular topologies, head-of-line blocking
35	Serge Autexier, Till Mossakowski	Integrating HOL-CASL into the Development Graph Manager MAYA.	FroCoS	2002	DBLP DOI BibTeX RDF
35	Christine Röckl, Daniel Hirschkoff, Stefan Berghofer	Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts.	FoSSaCS	2001	DBLP DOI BibTeX RDF
35	Ewen Denney	A Prototype Proof Translator from HOL to Coq.	TPHOLs	2000	DBLP DOI BibTeX RDF
35	Bruno Barras	Programming and Computing in HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
35	Jacques D. Fleuriot	On the Mechanization of Real Analysis in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
35	V. K. Pisini, Sofiène Tahar, Paul Curzon, Otmane Aït Mohamed, Xiaoyu Song	Formal hardware verification by integrating HOL and MDG.	ACM Great Lakes Symposium on VLSI	2000	DBLP DOI BibTeX RDF
35	Monica Nesi	Formalising a Value-Passing Calculus in HOL.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Meta-theoretic reasoning, Formal verification, Theorem proving, Higher order logic, Process calculi
35	Cornelia Pusch	Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL.	TACAS	1999	DBLP DOI BibTeX RDF
35	Sofiène Tahar, Paul Curzon, Jianping Lu	Three Approaches to Hardware Verification: HOL, MDG and VIS Compared.	FMCAD	1998	DBLP DOI BibTeX RDF
35	Haykal Tej, Burkhart Wolff	A Corrected Failure Divergence Model for CSP in Isabelle/HOL.	FME	1997	DBLP DOI BibTeX RDF
35	Amy P. Felty, Douglas J. Howe	Hybrid Interactive Theorem Proving Using Nuprl and HOL.	CADE	1997	DBLP DOI BibTeX RDF
35	Thomas Långbacka, Rimvydas Ruksenas, Joakim von Wright	TkWinHOL: A Tool for Window Inference in HOL.	TPHOLs	1995	DBLP DOI BibTeX RDF
35	Sten Agerholm, Michael J. C. Gordon	Experiments with ZF Set Theory in HOL and Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF