Search results for "HOL"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Johannes Åman Pohjola, Arve Gengelbach	A Mechanised Semantics for HOL with Ad-hoc Overloading.	LPAR	2020	DBLP DOI BibTeX RDF
16	Andreas Lochbihler, Ognjen Maric	Authenticated Data Structures as Functors in Isabelle/HOL.	FMBC@CAV	2020	DBLP DOI BibTeX RDF
16	Arve Gengelbach, Tjark Weber	Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading.	ICTAC	2020	DBLP DOI BibTeX RDF
16	Maria Ribeiro, Pedro Adão, Paulo Mateus	Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL.	Logic, Language, and Security	2020	DBLP DOI BibTeX RDF
16	Sebastian Reiche, Christoph Benzmüller	Public Announcement Logic in HOL.	DaLí	2020	DBLP DOI BibTeX RDF
16	Paulo Emílio de Vilhena, Lawrence C. Paulson	Algebraically Closed Fields in Isabelle/HOL.	IJCAR (2)	2020	DBLP DOI BibTeX RDF
16	Walter Guttmann	Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL.	IJCAR (2)	2020	DBLP DOI BibTeX RDF
16	Sohaib Soualah, Yousra Hafidi, Mohamed Khalgui, Allaoua Chaoui, Laïd Kahloul	Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop.	ICSOFT (Selected Papers)	2020	DBLP DOI BibTeX RDF
16	Sohaib Soualah, Yousra Hafidi, Mohamed Khalgui, Allaoua Chaoui, Laïd Kahloul	Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL.	ICSOFT	2020	DBLP DOI BibTeX RDF
16	Fabian Immler, Yong Kiam Tan	The Poincaré-Bendixson theorem in Isabelle/HOL.	CPP	2020	DBLP DOI BibTeX RDF
16	Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann	Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL.	NFM	2020	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Smart Induction for Isabelle/HOL (Tool Paper).	FMCAD	2020	DBLP DOI BibTeX RDF
16	Jonathan Julián Huerta y Munive	Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification.	SEFM	2020	DBLP DOI BibTeX RDF
16	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving.	CICM	2020	DBLP DOI BibTeX RDF
16	Laura Kovács, Hanna Lachnitt, Stefan Szeider	Formalizing Graph Trail Properties in Isabelle/HOL.	CICM	2020	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Simple Dataset for Proof Method Recommendation in Isabelle/HOL.	CICM	2020	DBLP DOI BibTeX RDF
16	Mathias Fleury	Formalization of logical calculi in Isabelle/HOL.		2020	RDF
16	Jonathan Julián Huerta y Munive	Algebraic verification of hybrid systems in Isabelle/HOL		2020	RDF
16	Wilayat Khan, David Sanán, Zhe Hou, Yang Liu 0003	On embedding a hardware description language in Isabelle/HOL.	Des. Autom. Embed. Syst.	2019	DBLP DOI BibTeX RDF
16	Lars Hupel	Certifying Dictionary Construction in Isabelle/HOL.	Fundam. Informaticae	2019	DBLP DOI BibTeX RDF
16	Jingzhi Zhang, Guohui Wang, Zhiping Shi 0002, Yong Guan, Yongdong Li	Formalization of functional variation in HOL Light.	J. Log. Algebraic Methods Program.	2019	DBLP DOI BibTeX RDF
16	Thomas Bittner	On the computational realization of formal ontologies: Formalizing an ontology of instantiation in spacetime using Isabelle/HOL as a case study.	Appl. Ontology	2019	DBLP DOI BibTeX RDF
16	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving.	IEEE Access	2019	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Ali Farjami, Paul Meder, Xavier Parent	I/O Logic in HOL.	FLAP	2019	DBLP BibTeX RDF
16	Yassmeen Elderhalli, Waqar Ahmad, Osman Hasan, Sofiène Tahar	Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving.	FLAP	2019	DBLP BibTeX RDF
16	Christoph Benzmüller, Ali Farjami, Xavier Parent	åqvist's Dyadic Deontic Logic E in HOL.	FLAP	2019	DBLP BibTeX RDF
16	Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel	From LCF to Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
16	Yutaka Nagashima	Towards Evolutionary Theorem Proving for Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
16	Yutaka Nagashima	LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
16	Jonathan Julián Huerta y Munive, Georg Struth	Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
16	Simon Foster 0001, Jonathan Julián Huerta y Munive, Georg Struth	Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
16	Waqar Ahmed, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar	On the Formalization of Importance Measures using HOL Theorem Proving.	CoRR	2019	DBLP BibTeX RDF
16	Mathias Fleury, Hans-Jörg Schurr	Reconstructing veriT Proofs in Isabelle/HOL.	PxTP	2019	DBLP DOI BibTeX RDF
16	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving.	CoRR	2019	DBLP BibTeX RDF
16	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams.	CoRR	2019	DBLP BibTeX RDF
16	Safouan Taha, Lina Ye, Burkhart Wolff	HOL-CSP Version 2.0.	Arch. Formal Proofs	2019	DBLP BibTeX RDF
16	Peter Lammich, Simon Wimmer 0001	IMP2 - Simple Program Verification in Isabelle/HOL.	Arch. Formal Proofs	2019	DBLP BibTeX RDF
16	Lars Hupel	A Verified Code Generator from Isabelle/HOL to CakeML.	Arch. Formal Proofs	2019	DBLP BibTeX RDF
16	Li-Ming Li, Zhi-Ping Shi 0002, Yong Guan, Qianying Zhang, Yong-Dong Li	Formalization of Geometric Algebra in HOL Light.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Ondrej Kuncar, Andrei Popescu 0001	A Consistent Foundation for Isabelle/HOL.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Peter Lammich	Refinement to Imperative HOL.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Wenda Li, Grant Olney Passmore, Lawrence C. Paulson	Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Mohammad Abdulaziz, Lawrence C. Paulson	An Isabelle/HOL Formalisation of Green's Theorem.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Peter Lammich, S. Reza Sefidgar	Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel	From LCF to Isabelle/HOL.	Formal Aspects Comput.	2019	DBLP DOI BibTeX RDF
16	Said Meghzili, Allaoua Chaoui, Martin Strecker, Elhillali Kerkouche	Verification of Model Transformations Using Isabelle/HOL and Scala.	Inf. Syst. Frontiers	2019	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.	APLAS	2019	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Towards evolutionary theorem proving for isabelle/HOL.	GECCO (Companion)	2019	DBLP DOI BibTeX RDF
16	Peter Lammich	Generating Verified LLVM from Isabelle/HOL.	ITP	2019	DBLP DOI BibTeX RDF
16	Manuel Eberl	Nine Chapters of Analytic Number Theory in Isabelle/HOL.	ITP	2019	DBLP DOI BibTeX RDF
16	Maximilian P. L. Haslbeck, Peter Lammich	Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL.	ITP	2019	DBLP DOI BibTeX RDF
16	Wenda Li, Lawrence C. Paulson	Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem.	CPP	2019	DBLP DOI BibTeX RDF
16	Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp	A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL.	CPP	2019	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette	Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk).	CPP	2019	DBLP DOI BibTeX RDF
16	Fabian Immler, Bohua Zhan	Smooth manifolds and types to sets for linear algebra in Isabelle/HOL.	CPP	2019	DBLP DOI BibTeX RDF
16	Waqar Ahmad, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar	On the formalization of importance measures using HOL theorem proving.	FormaliSE@ICSE	2019	DBLP DOI BibTeX RDF
16	Andreas Lööw, Magnus O. Myreen	A proof-producing translator for verilog development in HOL.	FormaliSE@ICSE	2019	DBLP DOI BibTeX RDF
16	Ralph Bottesch, Max W. Haslbeck, René Thiemann	Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL.	FroCos	2019	DBLP DOI BibTeX RDF
16	Yuhan Nie, Zhiping Shi 0002, Aixuan Wu, Ximeng Li 0003, Guohui Wang, Yong Guan	A HOL Theory of the Differential for Matrix Functions.	TASE	2019	DBLP DOI BibTeX RDF
16	Manuel Eberl	Verified Real Asymptotics in Isabelle/HOL.	ISSAC	2019	DBLP DOI BibTeX RDF
16	Alexander Maletzky	Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL.	CICM	2019	DBLP DOI BibTeX RDF
16	Lars Hupel	Verified Code Generation from Isabelle/HOL.		2019	RDF
16	Yiming Ouyang, Jianfeng Yang, Kun Xing, Zhengfeng Huang, Huaguo Liang	An improved communication scheme for non-HOL-blocking wireless NoC.	Integr.	2018	DBLP DOI BibTeX RDF
16	Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen	Programming and verifying a declarative first-order prover in Isabelle/HOL.	AI Commun.	2018	DBLP DOI BibTeX RDF
16	Adnan Rashid, Osman Hasan	Formalization of Lerch's Theorem using HOL Light.	FLAP	2018	DBLP BibTeX RDF
16	Sumayya Shiraz, Osman Hasan	A Library for Combinational Circuit Verification Using the HOL Theorem Prover.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2018	DBLP DOI BibTeX RDF
16	François Thiré	Sharing a Library between Proof Assistants: Reaching out to the HOL Family.	LFMTP@FSCD	2018	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Xavier Parent	I/O Logic in HOL - First Steps.	CoRR	2018	DBLP BibTeX RDF
16	Christoph Benzmüller, Ali Farjami, Xavier Parent	Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL.	CoRR	2018	DBLP BibTeX RDF
16	Jacques Carette, William M. Farmer, Patrick Laskowski	HOL Light QE.	CoRR	2018	DBLP BibTeX RDF
16	Wenda Li, Lawrence C. Paulson	Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL.	CoRR	2018	DBLP BibTeX RDF
16	Wenda Li, Lawrence C. Paulson	Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem.	CoRR	2018	DBLP BibTeX RDF
16	Adnan Rashid, Osman Hasan	Formalization of Lerch's Theorem using HOL Light.	CoRR	2018	DBLP BibTeX RDF
16	Alexander Maletzky, Fabian Immler	Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL.	CoRR	2018	DBLP BibTeX RDF
16	Yutaka Nagashima, Julian Parsert	Goal-Oriented Conjecturing for Isabelle/HOL.	CoRR	2018	DBLP BibTeX RDF
16	Artem Yushkovskiy, Stavros Tripakis	Comparison of Two Theorem Provers: Isabelle/HOL and Coq.	CoRR	2018	DBLP BibTeX RDF
16	Yu Zhang, Yongwang Zhao, David Sanán	A Verified Timsort C Implementation in Isabelle/HOL.	CoRR	2018	DBLP BibTeX RDF
16	Mnacho Echenim, Hervé Guiol, Nicolas Peltier	Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL.	CoRR	2018	DBLP BibTeX RDF
16	Ramana Kumar, Magnus O. Myreen	Clocked Definitions in HOL.	CoRR	2018	DBLP BibTeX RDF
16	Yutaka Nagashima, Yilun He	PaMpeR: Proof Method Recommendation System for Isabelle/HOL.	CoRR	2018	DBLP BibTeX RDF
16	Chun Tian 0001, Davide Sangiorgi	Unique Solutions of Contractions, CCS, and their HOL Formalisation.	EXPRESS/SOS	2018	DBLP DOI BibTeX RDF
16	Oliver Bracevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock, Markus Tasch	An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties.	Arch. Formal Proofs	2018	DBLP BibTeX RDF
16	Andreas Lochbihler, S. Reza Sefidgar	Constructive Cryptography in HOL.	Arch. Formal Proofs	2018	DBLP BibTeX RDF
16	Mohammad Abdulaziz, Lawrence C. Paulson	An Isabelle/HOL formalisation of Green's Theorem.	Arch. Formal Proofs	2018	DBLP BibTeX RDF
16	David Fuenmayor, Christoph Benzmüller	Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL.	Arch. Formal Proofs	2018	DBLP BibTeX RDF
16	Marco Maggesi	A Formalization of Metric Spaces in HOL Light.	J. Autom. Reason.	2018	DBLP DOI BibTeX RDF
16	Stefan Hallerstede	Tobias Nipkow and Gerwin Klein: Concrete Semantics with Isabelle/HOL - Springer Verlag, 2014, x + 289 pp, € 63, 29 (Hardback), ISBN 978-3-319-10542-0, http: //www.concrete-semantics.org/.	Formal Aspects Comput.	2018	DBLP DOI BibTeX RDF
16	Guohui Wang, Yong Guan, Zhiping Shi 0002, Qianying Zhang, Xiaojuan Li, Yongdong Li	Formalization of Symplectic Geometry in HOL-Light.	ICFEM	2018	DBLP DOI BibTeX RDF
16	Diego Marmsoler	A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL.	ICFEM	2018	DBLP DOI BibTeX RDF
16	Achim D. Brucker, Michael Herzberg	A Formal Semantics of the Core DOM in Isabelle/HOL.	WWW (Companion Volume)	2018	DBLP DOI BibTeX RDF
16	Cheikh Salmi, Mohamed Chaabani, Mohamed Mezghiche	A Formalized Procedure for Database Horizontal Fragmentation in Isabelle/HOL Proof Assistant.	MEDI	2018	DBLP DOI BibTeX RDF
16	Lars Hupel, Tobias Nipkow	A Verified Compiler from Isabelle/HOL to CakeML.	ESOP	2018	DBLP DOI BibTeX RDF
16	Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish	Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.	IJCAR	2018	DBLP DOI BibTeX RDF
16	Chantal Keller	Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL.	TAP@STAF	2018	DBLP DOI BibTeX RDF
16	Rachid Darbali-Zamora, Nicolas Cobo-Yepes, Eduardo I. Ortiz-Rivera, Erick E. Aponte-Bezares, Amilcar A. Rincon-Charris	Applying HOL/PBL to Prepare Undergraduate Students into Graduate Level Studies in the Field of Aerospace Engineering Using the Puerto Rico CubeSat Project Initiative.	FIE	2018	DBLP DOI BibTeX RDF
16	Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe	Physical Addressing on Real Hardware in Isabelle/HOL.	ITP	2018	DBLP DOI BibTeX RDF
16	Andreas Lochbihler	Fast Machine Words in Isabelle/HOL.	ITP	2018	DBLP DOI BibTeX RDF
16	Jacques Carette, William M. Farmer, Patrick Laskowski	HOL Light QE.	ITP	2018	DBLP DOI BibTeX RDF
16	Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples	Towards verifying ethereum smart contract bytecode in Isabelle/HOL.	CPP	2018	DBLP DOI BibTeX RDF
16	Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich	A verified SAT solver with watched literals using imperative HOL.	CPP	2018	DBLP DOI BibTeX RDF