Search results for "isabelle"

Hits ?▲	Authors	Title	Venue	Year	Link
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	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	Achim D. Brucker, Burkhart Wolff	Isabelle/DOF: Design and Implementation.	SEFM	2019	DBLP DOI BibTeX RDF
16	Manuel Eberl	Verified Real Asymptotics in Isabelle/HOL.	ISSAC	2019	DBLP DOI BibTeX RDF
16	Makarius Wenzel	Isabelle technology for the Archive of Formal Proofs with application to MMT.	CICM Workshops	2019	DBLP 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	Joshua Chen	Hybrid and alternative logics in Isabelle.	CICM Workshops	2019	DBLP BibTeX RDF
16	Makarius Wenzel	Interaction with Formal Mathematical Documents in Isabelle/PIDE.	CICM	2019	DBLP DOI BibTeX RDF
16	Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock	Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle.	CICM	2019	DBLP DOI BibTeX RDF
16	Sven Schneider 0001	Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle.		2019	RDF
16	Lars Hupel	Verified Code Generation from Isabelle/HOL.		2019	RDF
16	Ondrej Kuncar, Andrei Popescu 0001	Safety and conservativity of definitions in HOL and Isabelle/HOL.	Proc. ACM Program. Lang.	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	Bohua Zhan, Maximilian P. L. Haslbeck	Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle.	CoRR	2018	DBLP BibTeX RDF
16	Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry	Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle.	CoRR	2018	DBLP BibTeX RDF
16	Makarius Wenzel	Isabelle/jEdit as IDE for Domain-specific Formal Languages and Informal Text Documents.	F-IDE@FLoC	2018	DBLP DOI BibTeX RDF
16	Florian Kammüller	Attack Trees in Isabelle - CTL semantics, correctness and completeness.	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	Simon Foster 0001, James Baxter 0001, Ana Cavalcanti 0001, Alvaro Miyazawa, Jim Woodcock 0001	Automating Verification of State Machines with Reactive Designs and Isabelle/UTP.	CoRR	2018	DBLP BibTeX RDF
16	David Butler 0002, David Aspinall 0001, Adrià Gascón	How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation.	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	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	Yutaka Nagashima, Yilun He	PaMpeR: Proof Method Recommendation System for Isabelle/HOL.	CoRR	2018	DBLP 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	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	Peter Lammich, Simon Wimmer 0001	VerifyThis 2018 - Polished Isabelle Solutions.	Arch. Formal Proofs	2018	DBLP 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	Diego Marmsoler	A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL.	ICFEM	2018	DBLP DOI BibTeX RDF
16	Karol Pak	Mizar Set Comprehension in Isabelle Framework.	FedCSIS (Communication Papers)	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	Bohua Zhan, Maximilian P. L. Haslbeck	Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle.	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	Simon Foster 0001, James Baxter 0001, Ana Cavalcanti 0001, Alvaro Miyazawa, Jim Woodcock 0001	Automating Verification of State Machines with Reactive Designs and Isabelle/UTP.	FACS	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	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	Yutaka Nagashima, Yilun He	PaMpeR: proof method recommendation system for Isabelle/HOL.	ASE	2018	DBLP DOI BibTeX RDF
16	Florian Kammüller	Attack Trees in Isabelle.	ICICS	2018	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Karol Pak	Isabelle Import Infrastructure for the Mizar Mathematical Library.	CICM	2018	DBLP DOI BibTeX RDF
16	Achim D. Brucker, Idir Aït-Sadoune, Paolo Crisafulli, Burkhart Wolff	Using the Isabelle Ontology Framework - Linking the Formal with the Informal.	CICM	2018	DBLP DOI BibTeX RDF
16	Slawomir Kolodynski	IsarMathLib - a Formalized Mathematics Library for Isabelle/ZF.	CICM Workshops	2018	DBLP BibTeX RDF
16	Alexander Maletzky, Fabian Immler	Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL.	CICM	2018	DBLP DOI BibTeX RDF
16	Yutaka Nagashima, Julian Parsert	Goal-Oriented Conjecturing for Isabelle/HOL.	CICM	2018	DBLP DOI BibTeX RDF
16	Anders Schlichtkrull	Formalization of Logic in the Isabelle Proof Assistant.		2018	RDF
16	Jørgen Villadsen, Anders Schlichtkrull	Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant.	Trans. Large Scale Data Knowl. Centered Syst.	2017	DBLP DOI BibTeX RDF
16	Jørgen Villadsen, Alexander Birch Jensen, Anders Schlichtkrull	NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle.	FLAP	2017	DBLP BibTeX RDF
16	Jørgen Villadsen, Asta Halkjær From, Anders Schlichtkrull	Natural Deduction and the Isabelle Proof Assistant.	ThEdu@CADE	2017	DBLP DOI BibTeX RDF
16	Yutaka Nagashima	Towards Smart Proof Search for Isabelle.	CoRR	2017	DBLP BibTeX RDF
16	Stéphane Le Roux 0001, Érik Martin-Dorel, Jan-Georg Smaus	An Existence Theorem of Nash Equilibrium in Coq and Isabelle.	GandALF	2017	DBLP DOI BibTeX RDF
16	Ben Blumson	Anselm's God in Isabelle/HOL.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
16	Daniel Kirchner	Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
16	David Fuenmayor, Christoph Benzmüller	Types, Tableaus and Gödel's God in Isabelle/HOL.	Arch. Formal Proofs	2017	DBLP BibTeX RDF
16	Johannes Hölzl	Markov Chains and Markov Decision Processes in Isabelle/HOL.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
16	Manuel Eberl	Proving Divide and Conquer Complexities in Isabelle/HOL.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Karol Pak	Isabelle Formalization of Set Theoretic Structures and Set Comprehensions.	MACIS	2017	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Karol Pak	Progress in the Independent Certification of Mizar Mathematical Library in Isabelle.	FedCSIS	2017	DBLP DOI BibTeX RDF
16	Andreas Viktor Hess, Sebastian Mödersheim	Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL.	CSF	2017	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Jim Woodcock 0001	Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL.	Concurrency, Security, and Puzzles	2017	DBLP DOI BibTeX RDF
16	Ondrej Kuncar, Andrei Popescu 0001	Comprehending Isabelle/HOL's Consistency.	ESOP	2017	DBLP DOI BibTeX RDF
16	Mnacho Echenim, Nicolas Peltier	The Binomial Pricing Model in Finance: A Formalization in Isabelle.	CADE	2017	DBLP DOI BibTeX RDF
16	Yutaka Nagashima, Ramana Kumar	A Proof Strategy Language and Proof Script Generation for Isabelle/HOL.	CADE	2017	DBLP DOI BibTeX RDF
16	Albert Rizaldi, Jonas Keinholz, Monika Huber 0001, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, Tobias Nipkow	Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL.	IFM	2017	DBLP DOI BibTeX RDF
16	Sven Linker	Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL.	IFM	2017	DBLP DOI BibTeX RDF
16	Florian Kammüller, Juan Carlos Augusto, Simon Jones	Security and privacy requirements engineering for human centric IoT systems using eFRIEND and Isabelle.	SERA	2017	DBLP DOI BibTeX RDF
16	David Butler 0002, David Aspinall 0001, Adrià Gascón	How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation.	ITP	2017	DBLP DOI BibTeX RDF
16	Said Meghzili, Allaoua Chaoui, Martin Strecker, Elhillali Kerkouche	On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation Using Isabelle/HOL.	IRI	2017	DBLP DOI BibTeX RDF
16	Johannes Hölzl	Markov processes in Isabelle/HOL.	CPP	2017	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel	Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL.	FSCD	2017	DBLP DOI BibTeX RDF
16	Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis	Type Inference of Simulink Hierarchical Block Diagrams in Isabelle.	FORTE	2017	DBLP DOI BibTeX RDF
16	Florian Kammüller	A Proof Calculus for Attack Trees in Isabelle.	DPM/CBT@ESORICS	2017	DBLP DOI BibTeX RDF
16	Joseph R. Harrison	Towards an Isabelle/HOL formalisation of core Erlang.	Erlang Workshop	2017	DBLP DOI BibTeX RDF
16	Alexander Maletzky, Wolfgang Windsteiger	The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema.	CICM	2017	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Karol Pak	Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic.	CICM	2017	DBLP DOI BibTeX RDF
16	Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis	Type Inference of Simulink Hierarchical Block Diagrams in Isabelle.	CoRR	2016	DBLP BibTeX RDF
16	Jacques D. Fleuriot, Steven Obua, Phil Scott	Social Network Processes in the Isabelle and Coq Theorem Proving Communities.	CoRR	2016	DBLP BibTeX RDF
16	Yutaka Nagashima, Ramana Kumar	A Proof Strategy Language and Proof Script Generation for Isabelle.	CoRR	2016	DBLP BibTeX RDF
16	Lars Hupel, Viktor Kuncak	Translating Scala Programs to Isabelle/HOL.	CoRR	2016	DBLP BibTeX RDF
16	Christian Sternagel, Thomas Sternagel	Level-Confluence of 3-CTRSs in Isabelle/HOL.	CoRR	2016	DBLP BibTeX RDF
16	Julian Nagele, Vincent van Oostrom, Christian Sternagel	A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle.	CoRR	2016	DBLP BibTeX RDF
16	Zhe Hou, David Sanán, Alwen Tiu, Rajeev Goré, Ranald Clouston	Separata: Isabelle tactics for Separation Algebra.	Arch. Formal Proofs	2016	DBLP BibTeX RDF
16	Jesper Bengtson, Joachim Parrow, Tjark Weber	Psi-Calculi in Isabelle.	J. Autom. Reason.	2016	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban	A Learning-Based Fact Selector for Isabelle/HOL.	J. Autom. Reason.	2016	DBLP DOI BibTeX RDF
16	Daniel Matichuk, Toby C. Murray, Makarius Wenzel	Eisbach: A Proof Method Language for Isabelle.	J. Autom. Reason.	2016	DBLP DOI BibTeX RDF
16	Jesús Aransay, Jose Divasón	Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL.	Formal Aspects Comput.	2016	DBLP DOI BibTeX RDF
16	Florian Kammüller, Jason R. C. Nurse, Christian W. Probst	Attack Tree Analysis for Insider Threats on the IoT Using Isabelle.	HCI (20)	2016	DBLP DOI BibTeX RDF
16	Christoph Benzmüller, Dana S. Scott	Automating Free Logic in Isabelle/HOL.	ICMS	2016	DBLP DOI BibTeX RDF
16	Frank Zeyda, Simon Foster 0001, Leo Freitas	An Axiomatic Value Model for Isabelle/UTP.	UTP	2016	DBLP DOI BibTeX RDF
16	Lars Hupel, Viktor Kuncak	Translating Scala Programs to Isabelle/HOL - System Description.	IJCAR	2016	DBLP DOI BibTeX RDF
16	Viorel Preoteasa	Verifying Pointer Programs Using Separation Logic and Invariant Based Programming in Isabelle.	IFM	2016	DBLP DOI BibTeX RDF
16	Huazhen Xu, Zhen You, Jinyun Xue	Automatic verification of non-recursive algorithm of Hanoi Tower by using Isabelle Theorem Prover.	SNPD	2016	DBLP DOI BibTeX RDF
16	René Thiemann, Akihisa Yamada 0002	Algebraic Numbers in Isabelle/HOL.	ITP	2016	DBLP DOI BibTeX RDF