Search results for "HOL4"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
67	Aaron Richard Coble	Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover.	Privacy Enhancing Technologies	2008	DBLP DOI BibTeX RDF
40	Peter V. Homeier	The HOL-Omega Logic.	TPHOLs	2009	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
27	M. Saqib Nawaz, Muhammad Zohaib Nawaz, Osman Hasan, Philippe Fournier-Viger	Metaheuristic Algorithms for Proof Searching in HOL4.	SEKE	2022	DBLP DOI BibTeX RDF
27	Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, Mads Dam	Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution.	FMCAD	2022	DBLP DOI BibTeX RDF
27	Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar	Lassie: HOL4 Tactics by Example.	CoRR	2021	DBLP BibTeX RDF
27	M. Saqib Nawaz, Muhammad Zohaib Nawaz, Osman Hasan, Philippe Fournier-Viger, Meng Sun 0002	Proof searching and prediction in HOL4 with evolutionary/heuristic and deep learning techniques.	Appl. Intell.	2021	DBLP DOI BibTeX RDF
27	Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar	Lassie: HOL4 tactics by example.	CPP	2021	DBLP DOI BibTeX RDF
27	Thibault Gauthier	Tree Neural Networks in HOL4.	CoRR	2020	DBLP BibTeX RDF
27	Mohamed Abdelghany, Waqar Ahmad, Sofiène Tahar	A Formally Verified HOL4 Algebra for Event Trees.	CoRR	2020	DBLP BibTeX RDF
27	Muhammad Zohaib Nawaz, Osman Hasan, M. Saqib Nawaz, Philippe Fournier-Viger, Meng Sun 0002	Proof searching in HOL4 with genetic algorithm.	SAC	2020	DBLP DOI BibTeX RDF
27	Thibault Gauthier	Tree Neural Networks in HOL4.	CICM	2020	DBLP DOI BibTeX RDF
27	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	Integrating DFT and DRBD Formalizations in HOL4.	CoRR	2019	DBLP BibTeX RDF
27	Thibault Gauthier	Deep Reinforcement Learning in HOL4.	CoRR	2019	DBLP BibTeX RDF
27	Nadeem Iqbal, Osman Hasan, Umair Siddique, Falah Awwad	Formalization of Asymptotic Notations in HOL4.	ICCCS	2019	DBLP DOI BibTeX RDF
27	Fabian Immler, Jonas Rädle, Makarius Wenzel	Virtualization of HOL4 in Isabelle.	ITP	2019	DBLP DOI BibTeX RDF
27	Chunna Zhao, Shanshan Li	Formalization of fractional order PD control systems in HOL4.	Theor. Comput. Sci.	2018	DBLP DOI BibTeX RDF
27	Thibault Gauthier, Cezary Kaliszyk, Josef Urban	Learning to Reason with HOL4 tactics.	CoRR	2018	DBLP BibTeX RDF
27	Yassmeen Elderhalli, Waqar Ahmad, Osman Hasan, Sofiène Tahar	Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4.	CoRR	2018	DBLP BibTeX RDF
27	Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.	FMCAD	2018	DBLP DOI BibTeX RDF
27	Chun Tian 0001	Formalized Lambek Calculus in Higher Order Logic (HOL4).	CoRR	2017	DBLP BibTeX RDF
27	Chun Tian 0001	Further Formalization of the Process Algebra CCS in HOL4.	CoRR	2017	DBLP BibTeX RDF
27	Chun Tian 0001	A Formalization of the Process Algebra CCS in HOL4.	CoRR	2017	DBLP BibTeX RDF
27	Thibault Gauthier, Cezary Kaliszyk, Josef Urban	TacticToe: Learning to Reason with HOL4 Tactics.	LPAR	2017	DBLP DOI BibTeX RDF
27	Shanshan Li, Chunna Zhao, Yong Guan, Zhiping Shi 0002, Rui Wang 0024, Xiaojuan Li, Shiwei Ye	分数阶微积分定义的一致性在HOL4中的验证 (Formalization of Consistency of Fractional Calculus in HOL4).	计算机科学	2016	DBLP DOI BibTeX RDF
27	Thibault Gauthier, Cezary Kaliszyk	Premise Selection and External Provers for HOL4.	CoRR	2015	DBLP BibTeX RDF
27	Thibault Gauthier, Cezary Kaliszyk	Sharing HOL4 and HOL Light proof knowledge.	CoRR	2015	DBLP BibTeX RDF
27	Thibault Gauthier, Cezary Kaliszyk	Sharing HOL4 and HOL Light Proof Knowledge.	LPAR	2015	DBLP DOI BibTeX RDF
27	Anthony C. J. Fox	Improved Tool Support for Machine-Code Decompilation in HOL4.	ITP	2015	DBLP DOI BibTeX RDF
27	Thibault Gauthier, Cezary Kaliszyk	Premise Selection and External Provers for HOL4.	CPP	2015	DBLP DOI BibTeX RDF
27	Osman Hasan, Syed Ali Khayam	Towards Formal Linear Cryptanalysis using HOL4.	J. Univers. Comput. Sci.	2014	DBLP DOI BibTeX RDF
27	Aditi Barthwal, Michael Norrish	A mechanisation of some context-free language theory in HOL4.	J. Comput. Syst. Sci.	2014	DBLP DOI BibTeX RDF
27	Diego Machado Dias, Juliano Iyoda	Compositionality and correctness of fault tolerant patterns in HOL4.	Sci. Comput. Program.	2014	DBLP DOI BibTeX RDF
27	Liming Li, Zhiping Shi 0002, Yong Guan, Chunna Zhao, Jie Zhang 0074, Hongxing Wei	Formal verification of a collision-free algorithm of dual-arm robot in HOL4.	ICRA	2014	DBLP DOI BibTeX RDF
27	Liming Li, Zhiping Shi 0002, Yong Guan, Jie Zhang 0074, Hongxing Wei	Formalizing the Matrix Inversion Based on the Adjugate Matrix in HOL4.	Intelligent Information Processing	2014	DBLP DOI BibTeX RDF
27	Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish	Beagle as a HOL4 external ATP method.	PAAR@IJCAR	2014	DBLP DOI BibTeX RDF
27	Sohaib Ahmad, Osman Hasan, Umair Siddique, Sofiène Tahar	Formalization of Zsyntax to Reason About Molecular Pathways in HOL4.	SBMF	2014	DBLP DOI BibTeX RDF
27	Zhiping Shi 0002, Weiqing Gu, Xiaojuan Li, Yong Guan, Shiwei Ye, Jie Zhang 0074, Hongxing Wei	The Gauge Integral Theory in HOL4.	J. Appl. Math.	2013	DBLP DOI BibTeX RDF
27	Ramana Kumar	Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4.	PxTP@CADE	2013	DBLP DOI BibTeX RDF
27	Michael J. C. Gordon, Matt Kaufmann, Sandip Ray	The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4.	J. Autom. Reason.	2011	DBLP DOI BibTeX RDF
27	Ramana Kumar, Tjark Weber	Validating QBF Validity in HOL4.	ITP	2011	DBLP DOI BibTeX RDF
27	Anthony C. J. Fox	LCF-Style Bit-Blasting in HOL4.	ITP	2011	DBLP DOI BibTeX RDF
27	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
27	Tjark Weber	Validating QBF Invalidity in HOL4.	ITP	2010	DBLP DOI BibTeX RDF
27	Aditi Barthwal, Michael Norrish	A Formalisation of the Normal Forms of Context-Free Grammars in HOL4.	CSL	2010	DBLP DOI BibTeX RDF
27	James Reynolds	An automatic proof-generating translation from higher-order to first-order logic : with applications to linking HOL4 and ACL2.		2009	RDF
27	Konrad Slind, Michael Norrish	A Brief Overview of HOL4.	TPHOLs	2008	DBLP DOI BibTeX RDF
20	Magnus O. Myreen	Verified just-in-time compiler on x86.	POPL	2010	DBLP DOI BibTeX RDF	self-modifying code, just in time, compiler verification
20	Scott Owens, Susmit Sarkar, Peter Sewell	A Better x86 Memory Model: x86-TSO.	TPHOLs	2009	DBLP DOI BibTeX RDF
20	Magnus O. Myreen, Michael J. C. Gordon	Verified LISP Implementations on ARM, x86 and PowerPC.	TPHOLs	2009	DBLP DOI BibTeX RDF
20	Tom Ridge	Verifying distributed systems: the operational approach.	POPL	2009	DBLP DOI BibTeX RDF	ground and symbolic evaluation, hoare-style assertions, persistent queue, rely/guarantee, distributed, refinement, invariants, network protocol, operational semantics, infrastructure, separation, linearizability, hol, ocaml, local reasoning, inductive reasoning
20	Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon	Extensible Proof-Producing Compilation.	CC	2009	DBLP DOI BibTeX RDF
20	Jens Brandt 0001, Klaus Schneider 0001	Formal Reasoning About Causality Analysis.	TPHOLs	2008	DBLP DOI BibTeX RDF
20	Mike Gordon	Twenty Years of Theorem Proving for HOLs Past, Present and Future.	TPHOLs	2008	DBLP DOI BibTeX RDF
20	Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon	Proof producing synthesis of arithmetic and cryptographic hardware.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Cryptography, Compiling, Theorem proving, Hardware synthesis, High assurance
20	James Reynolds	Automatically Translating Type and Function Definitions from HOL to ACL2.	TPHOLs	2007	DBLP DOI BibTeX RDF
20	Christoph Benzmüller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier	Deep Inference for Automated Proof Tutoring?	KI	2007	DBLP DOI BibTeX RDF
20	Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon	Hoare Logic for ARM Machine Code.	FSEN	2007	DBLP DOI BibTeX RDF
20	Magnus O. Myreen, Michael J. C. Gordon	Hoare Logic for Realistically Modelled Machine Code.	TACAS	2007	DBLP DOI BibTeX RDF
20	John Harrison 0001, Konrad Slind, Rob Arthan	HOL.	The Seventeen Provers of the World	2006	DBLP DOI BibTeX RDF
20	Anduo Wang, Fei He 0001, Ming Gu 0001, Xiaoyu Song	Verifying Java Programs By Theorem Prover HOL.	COMPSAC (1)	2006	DBLP DOI BibTeX RDF
20	Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann	An Integration of HOL and ACL2.	FMCAD	2006	DBLP DOI BibTeX RDF
20	Paola Inverardi, Fabio Mancinelli, Monica Nesi	A declarative framework for adaptable applications in heterogeneous environments.	SAC	2004	DBLP DOI BibTeX RDF