Search results for "isabelle"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Christoph Benzmüller, David Fuenmayor	Value-Oriented Legal Argumentation in Isabelle/HOL.	ITP	2021	DBLP DOI BibTeX RDF
16	Joshua Chen	Homotopy Type Theory in Isabelle.	ITP	2021	DBLP DOI BibTeX RDF
16	Max W. Haslbeck, René Thiemann	An Isabelle/HOL formalization of AProVE's termination method for LLVM IR.	CPP	2021	DBLP DOI BibTeX RDF
16	Sophie Tourret, Jasmin Blanchette	A modular Isabelle framework for verifying saturation provers.	CPP	2021	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Chung-Kil Hur, Jim Woodcock 0001	Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL.	CONCUR	2021	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Faster Smarter Proof by Induction in Isabelle/HOL.	IJCAI	2021	DBLP DOI BibTeX RDF
16	Diego Marmsoler, Achim D. Brucker	A Denotational Semantics of Solidity in Isabelle/HOL.	SEFM	2021	DBLP DOI BibTeX RDF
16	Stepan Holub	Computing the Border Array in Isabelle/HOL (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
16	Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Erik Sturzenhecker	Beautiful Formalizations in Isabelle/Naproche.	CICM	2021	DBLP DOI BibTeX RDF
16	Martin Raska, Stepán Starosta	Producing Symmetrical Facts for lIsts induced by the List Reversal Mapping in Isabelle/HOL (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
16	Fabian Huch	Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs - Extended Abstract (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
16	Asta Halkjær From, Agnes Moesgård Eschen, Jørgen Villadsen	Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL.	CICM	2021	DBLP DOI BibTeX RDF
16	Alfio Ricardo de Brito Martini	Reasoning about Partial Correctness Assertions in Isabelle/HOL.	RITA	2020	DBLP DOI BibTeX RDF
16	Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf	Formalization of Forcing in Isabelle/ZF.	CoRR	2020	DBLP BibTeX RDF
16	Simon Foster 0001, Yakoub Nemouchi, Mario Gleirscher, Ran Wei, Tim Kelly	Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description).	CoRR	2020	DBLP BibTeX RDF
16	Sadegh Dalvandi, Brijesh Dongol, Simon Doherty	Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	Smart Induction for Isabelle/HOL (System Description).	CoRR	2020	DBLP BibTeX RDF
16	Florian Kammüller, Manfred Kerber	Applying the Isabelle Insider Framework to Airplane Security.	CoRR	2020	DBLP BibTeX RDF
16	Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn	Isabelle/HOL as a Meta-Language for Teaching Logic.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
16	Anthony Bordg, Hanna Lachnitt, Yijun He	Certified Quantum Computation in Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Michael Kohlhase, Florian Rabe 0001, Makarius Wenzel	Making Isabelle Content Accessible in Knowledge Representation Formats.	CoRR	2020	DBLP BibTeX RDF
16	Walther Neuper	Lucas-Interpretation on Isabelle's Functions.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Towards United Reasoning for Automatic Induction in Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL.	CoRR	2020	DBLP BibTeX RDF
16	Yutaka Nagashima	Faster Smarter Induction in Isabelle/HOL with SeLFiE.	CoRR	2020	DBLP BibTeX RDF
16	Florian Kammüller	A Formal Development Cycle for Security Engineering in Isabelle.	CoRR	2020	DBLP BibTeX RDF
16	Filip Maric, Sana Stojanovic-Durdevic	Formalizing IMO Problems and Solutions in Isabelle/HOL.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
16	Florian Kammueller	Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
16	Salomon Sickert	An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
16	Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf	Formalization of Forcing in Isabelle/ZF.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
16	Anthony Bordg, Hanna Lachnitt, Yijun He	Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
16	René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada 0002	Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002	A Verified Implementation of Algebraic Numbers in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Mnacho Echenim, Hervé Guiol, Nicolas Peltier	Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Wenda Li, Lawrence C. Paulson	Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
16	Simon Foster 0001, James Baxter 0001, Ana Cavalcanti 0001, Jim Woodcock 0001, Frank Zeyda	Unifying semantic foundations for automated verification tools in Isabelle/UTP.	Sci. Comput. Program.	2020	DBLP DOI BibTeX RDF
16	Jens Christoph Bürger, Hendrik Kausch, Deni Raco, Jan Oliver Ringert, Bernhard Rumpe, Sebastian Stüber, Marc Wiartalla	Towards an Isabelle Theory for distributed, interactive systems: The untimed case. (PDF / PS)		2020	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.	RAMiCS	2020	DBLP DOI BibTeX RDF
16	Florian Kammüller, Uwe Nestmann	Inter-Blockchain Protocols with the Isabelle Infrastructure Framework.	FMBC@CAV	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	Jørgen Villadsen	Tautology Checkers in Isabelle and Haskell.	CILC	2020	DBLP BibTeX RDF
16	Changjing Wang, Fan Xu, Haimei Luo, Qing Huang, Zhengkang Zuo	Development Method of Three Kinds of Typical Tree Structure Algorithms and Isabelle-based Machine Assisted Verification.	QRS	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	Paulo Emílio de Vilhena, Lawrence C. Paulson	Algebraically Closed Fields in Isabelle/HOL.	IJCAR (2)	2020	DBLP DOI BibTeX RDF
16	Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf	Formalization of Forcing in Isabelle/ZF.	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	Florian Kammüller, Bianca Lutz	Modeling and Analyzing the Corona-Virus Warning App with the Isabelle Infrastructure Framework.	DPM/CBT@ESORICS	2020	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Smart Induction for Isabelle/HOL (Tool Paper).	FMCAD	2020	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Yakoub Nemouchi, Colin O'Halloran, Karen Stephenson, Nick Tudor	Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study.	FormaliSE@ICSE	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	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	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	Makarius Wenzel	Interaction with Formal Mathematical Documents in Isabelle/PIDE.	CoRR	2019	DBLP BibTeX RDF
16	Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel	From LCF to Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
16	Yakoub Nemouchi, Simon Foster 0001, Mario Gleirscher, Tim Kelly	Mechanised Assurance Cases with Integrated Formal Methods in Isabelle.	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	Joshua Chen	An Implementation of Homotopy Type Theory in Isabelle/Pure.	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	Frédéric Tuong, Burkhart Wolff	Deeply Integrating C11 Code Support into Isabelle/PIDE.	F-IDE@FM	2019	DBLP DOI BibTeX RDF
16	Florian Kammüller	QKD in Isabelle - Bayesian Calculation.	CoRR	2019	DBLP BibTeX RDF
16	Makarius Wenzel	Isabelle technology for the Archive of Formal Proofs.	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	Simon Foster 0001, James Baxter 0001, Ana Cavalcanti 0001, Jim Woodcock 0001, Frank Zeyda	Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP.	CoRR	2019	DBLP BibTeX RDF
16	Florian Kammüller	Attack trees in Isabelle extended with probabilities for quantum cryptography.	Comput. Secur.	2019	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Frank Zeyda, Yakoub Nemouchi, Pedro Ribeiro 0002, Burkhart Wolff	Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming.	Arch. Formal Proofs	2019	DBLP BibTeX RDF
16	Peter Lammich, Simon Wimmer 0001	VerifyThis 2019 - Polished Isabelle Solutions.	Arch. Formal Proofs	2019	DBLP BibTeX RDF
16	Frédéric Tuong, Burkhart Wolff	Isabelle/C.	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	Ondrej Kuncar, Andrei Popescu 0001	A Consistent Foundation for Isabelle/HOL.	J. Autom. Reason.	2019	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Karol Pak	Semantics of Mizar as an Isabelle Object Logic.	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	Simon Foster 0001	Hybrid Relations in Isabelle/UTP.	UTP	2019	DBLP DOI BibTeX RDF
16	Michael Kohlhase, Florian Rabe 0001, Makarius Wenzel	Making Isabelle Content Accessible in Knowledge Representation Formats.	TYPES	2019	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Towards evolutionary theorem proving for isabelle/HOL.	GECCO (Companion)	2019	DBLP DOI BibTeX RDF
16	Yakoub Nemouchi, Simon Foster 0001, Mario Gleirscher, Tim Kelly	Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods.	IFM	2019	DBLP DOI BibTeX RDF
16	Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher	The DPRM Theorem in Isabelle (Short Paper).	ITP	2019	DBLP DOI BibTeX RDF
16	Peter Lammich	Generating Verified LLVM from Isabelle/HOL.	ITP	2019	DBLP DOI BibTeX RDF
16	Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry	Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle.	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	Fabian Immler, Jonas Rädle, Makarius Wenzel	Virtualization of HOL4 in Isabelle.	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