Search results for "hol"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
16	Christoph Benzmüller	HOL Provers for First-order Modal Logics - Experiments.	ARQNL@IJCAR	2014	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, Andrei Popescu 0001, Dmitriy Traytel	Cardinals in Isabelle/HOL.	ITP	2014	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu 0001, Dmitriy Traytel	Truly Modular (Co)datatypes for Isabelle/HOL.	ITP	2014	DBLP DOI BibTeX RDF
16	Rob Arthan	HOL Constant Definition Done Right.	ITP	2014	DBLP DOI BibTeX RDF
16	Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens	HOL with Definitions: Semantics, Soundness, and a Verified Implementation.	ITP	2014	DBLP DOI BibTeX RDF
16	Vincent Aravantinos, Sofiène Tahar	Implicational Rewriting Tactics in HOL.	ITP	2014	DBLP DOI BibTeX RDF
16	Umair Siddique, Mohamed Yousri Mahmoud, Sofiène Tahar	On the Formalization of Z-Transform in HOL.	ITP	2014	DBLP DOI BibTeX RDF
16	Mohamed Yousri Mahmoud, Sofiène Tahar	On the Quantum Formalization of Coherent Light in HOL.	NASA Formal Methods	2014	DBLP DOI BibTeX RDF
16	Sohaib Ahmad, Osman Hasan, Umair Siddique	Towards Formal Reasoning about Molecular Pathways in HOL.	WETICE	2014	DBLP DOI BibTeX RDF
16	Jesús Aransay-Azofra, Jose Divasón, Jónathan Heras, Laureano Lambán, María Vico Pascual, Ángel Luis Rubio, Julio Rubio 0001	Obtaining an ACL2 Specification from an Isabelle/HOL Theory.	AISC	2014	DBLP DOI BibTeX RDF
16	Alasdair Armstrong, Victor B. F. Gomes, Georg Struth	Lightweight Program Construction and Verification Tools in Isabelle/HOL.	SEFM	2014	DBLP DOI BibTeX RDF
16	Thibault Gauthier, Cezary Kaliszyk	Matching Concepts across HOL Libraries.	CICM	2014	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Florian Rabe 0001	Towards Knowledge Management for HOL Light.	CICM	2014	DBLP DOI BibTeX RDF
16	Liya Liu, Osman Hasan, Sofiène Tahar	Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL.	J. Comput. Sci. Technol.	2013	DBLP DOI BibTeX RDF
16	Tarek Mhamdi, Osman Hasan, Sofiène Tahar	Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL.	ACM Trans. Embed. Comput. Syst.	2013	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Josef Urban	Lemma Mining over HOL Light.	CoRR	2013	DBLP BibTeX RDF
16	Steven Obua, Mark Adams, David Aspinall 0001	Capturing Hiproofs in HOL Light.	CoRR	2013	DBLP BibTeX RDF
16	Christoph Benzmueller, Bruno Woltzenlogel Paleo	Gödel's God in Isabelle/HOL.	Arch. Formal Proofs	2013	DBLP BibTeX RDF
16	Maria Spichkova	Stream Processing Components: Isabelle/HOL Formalisation and Case Studies.	Arch. Formal Proofs	2013	DBLP BibTeX RDF
16	John Harrison 0001	The HOL Light Theory of Euclidean Space.	J. Autom. Reason.	2013	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Josef Urban	Lemma Mining over HOL Light.	LPAR	2013	DBLP DOI BibTeX RDF
16	Syeda Hira Taqdees, Osman Hasan	Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light.	LPAR	2013	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Thomas Raths	HOL Based First-Order Modal Logic Provers.	LPAR	2013	DBLP DOI BibTeX RDF
16	Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel, Burkhart Wolff	The Circus Testing Theory Revisited in Isabelle/HOL.	ICFEM	2013	DBLP DOI BibTeX RDF
16	Achim D. Brucker, Lukas Brügger, Burkhart Wolff	hol-TestGen/fw - An Environment for Specification-Based Firewall Conformance Testing.	ICTAC	2013	DBLP DOI BibTeX RDF
16	Osman Hasan, Muhammad Ahmad	Formal analysis of steady state errors in feedback control systems using HOL-light.	DATE	2013	DBLP DOI BibTeX RDF
16	Pedro Yebenes Segura, Jesús Escudero-Sahuquillo, Crispín Gómez Requena, Pedro Javier García, Francisco J. Quiles 0001, José Duato	BBQ: A Straightforward Queuing Scheme to Reduce HoL-Blocking in High-Performance Hybrid Networks.	Euro-Par	2013	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Josef Urban	PRocH: Proof Reconstruction for HOL Light.	CADE	2013	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Thomas Sternagel	Initial Experiments on Deriving a Complete HOL Simplification Set.	PxTP@CADE	2013	DBLP DOI BibTeX RDF
16	Roberto Peñaranda, Crispín Gómez Requena, María Engracia Gómez, Pedro López 0001, José Duato	Deterministic Routing with HoL-Blocking-Awareness for Direct Topologies.	ICCS	2013	DBLP DOI BibTeX RDF
16	Magnus O. Myreen, Scott Owens, Ramana Kumar	Steps towards Verified Implementations of HOL Light.	ITP	2013	DBLP DOI BibTeX RDF
16	Jian Xu, Xingyuan Zhang, Christian Urban	Mechanising Turing Machines and Computability Theory in Isabelle/HOL.	ITP	2013	DBLP DOI BibTeX RDF
16	Florian Haftmann, Alexander Krauss 0001, Ondrej Kuncar, Tobias Nipkow	Data Refinement in Isabelle/HOL.	ITP	2013	DBLP DOI BibTeX RDF
16	Michael Norrish, Brian Huffman	Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1.	ITP	2013	DBLP DOI BibTeX RDF
16	Alasdair Armstrong, Georg Struth, Tjark Weber	Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL.	ITP	2013	DBLP DOI BibTeX RDF
16	Liya Liu, Osman Hasan, Vincent Aravantinos, Sofiène Tahar	Formal Reasoning about Classified Markov Chains in HOL.	ITP	2013	DBLP DOI BibTeX RDF
16	Johannes Hölzl, Fabian Immler, Brian Huffman	Type Classes and Filters for Mathematical Analysis in Isabelle/HOL.	ITP	2013	DBLP DOI BibTeX RDF
16	Brian Huffman, Ondrej Kuncar	Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL.	CPP	2013	DBLP DOI BibTeX RDF
16	Andreas Schropp, Andrei Popescu 0001	Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory.	CPP	2013	DBLP DOI BibTeX RDF
16	Christoph Benzmueller	Automating Quantified Conditional Logics in HOL.	IJCAI	2013	DBLP BibTeX RDF
16	Alfio Martini	Programming Language Semantics with Isabelle/HOL.	WEIT	2013	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Josef Urban	Automated Reasoning Service for HOL Light.	MKM/Calculemus/DML	2013	DBLP DOI BibTeX RDF
16	Steven Obua, Mark Adams, David Aspinall 0001	Capturing Hiproofs in HOL Light.	MKM/Calculemus/DML	2013	DBLP DOI BibTeX RDF
16	D. N. T. Kumar, Qufu Wei	A General Computational Framework and Simulations of Branching Programs of Boolean Circuits Using Higher Order Logic (HOL) Software - An Insight into ECAD Tool Design Paradigm.	Comput. Inf. Sci.	2012	DBLP DOI BibTeX RDF
16	Gilles Dowek, Murdoch James Gabbay	PNL to HOL: From the logic of nominal sets to the logic of higher-order functions.	Theor. Comput. Sci.	2012	DBLP DOI BibTeX RDF
16	Christoph Benzmueller, Valerio Genovese	Quantified Conditional Logics are Fragments of HOL	CoRR	2012	DBLP BibTeX RDF
16	Peter Lammich, Rene Meis	A Separation Logic Framework for Imperative HOL.	Arch. Formal Proofs	2012	DBLP BibTeX RDF
16	Stefan Berghofer	A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL.	J. Autom. Reason.	2012	DBLP DOI BibTeX RDF
16	Tobias Nipkow	Interactive Proof: Introduction to Isabelle/HOL.	Software Safety and Security	2012	DBLP DOI BibTeX RDF
16	Umair Siddique, Vincent Aravantinos, Sofiène Tahar	On the Formal Analysis of Geometrical Optics in HOL.	Automated Deduction in Geometry	2012	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Josef Urban	Initial Experiments with External Provers and Premise Selection on HOL Light Corpora.	PAAR@IJCAR	2012	DBLP DOI BibTeX RDF
16	Roberto Peñaranda, Crispín Gómez Requena, María Engracia Gómez, Pedro López 0001, José Duato	IODET: A HoL-blocking-aware Deterministic Routing Algorithm for Direct Topologies.	ICPADS	2012	DBLP DOI BibTeX RDF
16	Achim D. Brucker, Burkhart Wolff	Featherweight OCL: a study for the consistent semantics of OCL 2.3 in HOL.	OCL@MoDELS	2012	DBLP DOI BibTeX RDF
16	Fabian Immler, Johannes Hölzl	Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL.	ITP	2012	DBLP DOI BibTeX RDF
16	Yongjian Li, William N. N. Hung, Xiaoyu Song	A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL.	Theor. Comput. Sci.	2011	DBLP DOI BibTeX RDF
16	Tjark Weber	SMT solvers: new oracles for the HOL theorem prover.	Int. J. Softw. Tools Technol. Transf.	2011	DBLP DOI BibTeX RDF
16	Gudmund Grov, Stephan Merz	A Definitional Encoding of TLA* in Isabelle/HOL.	Arch. Formal Proofs	2011	DBLP BibTeX RDF
16	Simon Foster 0001, Georg Struth, Tjark Weber	Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial).	RAMiCS	2011	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Christian Urban	Quotients revisited for Isabelle/HOL.	SAC	2011	DBLP DOI BibTeX RDF
16	Liya Liu, Osman Hasan, Sofiène Tahar	Formalization of Finite-State Discrete-Time Markov Chains in HOL.	ATVA	2011	DBLP DOI BibTeX RDF
16	Johannes Hölzl, Armin Heller	Three Chapters of Measure Theory in Isabelle/HOL.	ITP	2011	DBLP DOI BibTeX RDF
16	Tarek Mhamdi, Osman Hasan, Sofiène Tahar	Formalization of Entropy Measures in HOL.	ITP	2011	DBLP DOI BibTeX RDF
16	Ondrej Kuncar	Proving Valid Quantified Boolean Formulas in HOL Light.	ITP	2011	DBLP DOI BibTeX RDF
16	Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber	Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.	CPP	2011	DBLP DOI BibTeX RDF
16	Umair Siddique, Osman Hasan	Formal analysis of fractional order systems in HOL.	FMCAD	2011	DBLP BibTeX RDF
16	Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow	Automatic Proof and Disproof in Isabelle/HOL.	FroCoS	2011	DBLP DOI BibTeX RDF
16	Robbert Krebbers, Freek Wiedijk	A Formalization of the C99 Standard in HOL, Isabelle and Coq.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
16	Thomas Tuerk	A separation logic framework for HOL.		2011	RDF
16	Ludovic Henrio, Muhammad Uzair Khan	Asynchronous Components with Futures: Semantics and Proofs in Isabelle/HOL.	FESCA@ETAPS	2010	DBLP DOI BibTeX RDF
16	Filip Maric	Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL.	Theor. Comput. Sci.	2010	DBLP DOI BibTeX RDF
16	Teresa Nachiondo Frinós, José Flich, José Duato	Buffer Management Strategies to Reduce HoL Blocking.	IEEE Trans. Parallel Distributed Syst.	2010	DBLP DOI BibTeX RDF	distributed systems, network operating systems, computer systems organization, network architecture and design, Communication/networking and information technology
16	Sascha Böhme, Michal Moskal, Wolfram Schulte, Burkhart Wolff	HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler.	J. Autom. Reason.	2010	DBLP DOI BibTeX RDF
16	Behzad Akbarpour, Amr T. Abdel-Hamid, Sofiène Tahar, John Harrison 0001	Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL.	Comput. J.	2010	DBLP DOI BibTeX RDF
16	Jacques D. Fleuriot	Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL.	Automated Deduction in Geometry	2010	DBLP DOI BibTeX RDF
16	Petros Papapanagiotou, Jacques D. Fleuriot	An Isabelle-Like Procedural Mode for HOL Light.	LPAR (Yogyakarta)	2010	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette	Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod.	LPAR short papers(Yogyakarta)	2010	DBLP DOI BibTeX RDF
16	Mark Adams	Introducing HOL Zero - (Extended Abstract).	ICMS	2010	DBLP DOI BibTeX RDF
16	Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff	Unifying Theories in Isabelle/HOL.	UTP	2010	DBLP DOI BibTeX RDF
16	Laura I. Meikle, Jacques D. Fleuriot	Automation for Geometry in Isabelle/HOL.	PAAR@IJCAR	2010	DBLP DOI BibTeX RDF
16	Chantal Keller, Benjamin Werner	Importing HOL Light into Coq.	ITP	2010	DBLP DOI BibTeX RDF
16	Tarek Mhamdi, Osman Hasan, Sofiène Tahar	On the Formalization of the Lebesgue Integration Theory in HOL.	ITP	2010	DBLP DOI BibTeX RDF
16	Douglas J. Howe	Higher-Order Abstract Syntax in Isabelle/HOL.	ITP	2010	DBLP DOI BibTeX RDF
16	Florian Kammüller, Alexander Rein, Mark-Oliver Reiser	Feature link propagation across variability representations with Isabelle/HOL.	PLEASE@ICSE	2010	DBLP DOI BibTeX RDF
16	Maksym Bortin, Christoph Lüth	Structured Formal Development with Quotient Types in Isabelle/HOL.	AISC/MKM/Calculemus	2010	DBLP DOI BibTeX RDF
16	Alejandro Martínez, Pedro Javier García, Francisco José Alfaro, José L. Sánchez 0002, José Flich, Francisco J. Quiles 0001, José Duato	A Switch Architecture Guaranteeing QoS Provision and HOL Blocking Elimination.	IEEE Trans. Parallel Distributed Syst.	2009	DBLP DOI BibTeX RDF
16	Freek Wiedijk	Stateless HOL	TYPES	2009	DBLP DOI BibTeX RDF
16	Tjark Weber, Hasan Amjad	Efficiently checking propositional refutations in HOL theorem provers.	J. Appl. Log.	2009	DBLP DOI BibTeX RDF
16	Bart Kastermans	An Example of a Cofinitary Group in Isabelle/HOL.	Arch. Formal Proofs	2009	DBLP BibTeX RDF
16	Tobias Nipkow	Social Choice Theory in HOL.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF
16	Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu 0001	Theory support for weak higher order abstract syntax in Isabelle/HOL.	LFMTP	2009	DBLP DOI BibTeX RDF
16	Christian Doczkal, Jan Schwinghammer	Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal.	LFMTP	2009	DBLP DOI BibTeX RDF
16	Christophe Raffalli, Frédéric Ruyer	Realizability of the Axiom of Choice in HOL. (An Analysis of Krivine's Work).	Fundam. Informaticae	2008	DBLP BibTeX RDF
16	Robert L. Constable, Wojciech Moczydlowski	Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics	CoRR	2008	DBLP BibTeX RDF
16	Robert L. Constable, Wojciech Moczydlowski	Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics.	Log. Methods Comput. Sci.	2008	DBLP DOI BibTeX RDF
16	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	The Performance of Combining Multiway Decision Graphs and HOL Theorem Prover.	FDL	2008	DBLP DOI BibTeX RDF
16	Achim D. Brucker, Burkhart Wolff	HOL-OCL: A Formal Proof Environment for UML/OCL.	FASE	2008	DBLP DOI BibTeX RDF	holocl, ocl, Formal Method, Theorem Proving, uml
16	Tom Maertens, Joris Walraevens, Herwig Bruneel	A modified HOL priority scheduling discipline: Performance analysis.	Eur. J. Oper. Res.	2007	DBLP DOI BibTeX RDF
16	Behzad Akbarpour, Sofiène Tahar	Error analysis of digital filters using HOL theorem proving.	J. Appl. Log.	2007	DBLP DOI BibTeX RDF
16	Lukas Bulwahn, Alexander Krauss 0001, Tobias Nipkow	Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL.	TPHOLs	2007	DBLP DOI BibTeX RDF
16	Lars Gesellensetter, Sabine Glesner, Elke Salecker	Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler.	FMICS	2007	DBLP DOI BibTeX RDF