Search results for "isabelle"

Hits ?▲	Authors	Title	Venue	Year	Link
16	Mohammad Abdulaziz, Lawrence C. Paulson	An Isabelle/HOL Formalisation of Green's Theorem.	ITP	2016	DBLP DOI BibTeX RDF
16	René Thiemann, Akihisa Yamada 0002	Formalizing jordan normal forms in Isabelle/HOL.	CPP	2016	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Karol Pak, Josef Urban	Towards a mizar environment for isabelle: foundations and language.	CPP	2016	DBLP DOI BibTeX RDF
16	Alexander Steen, Max Wisniewski, Christoph Benzmüller	Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL.	GCAI	2016	DBLP DOI BibTeX RDF
16	Florian Kammüller	Isabelle Modelchecking for Insider Threats.	DPM/QASA@ESORICS	2016	DBLP DOI BibTeX RDF
16	Xiaojun Ji, Lihua Song	Mutual Exclusion Verification of Peterson's Solution in Isabelle/HOL.	TSA	2016	DBLP DOI BibTeX RDF
16	Viorel Preoteasa, Ralph-Johan Back, Johannes Eriksson	Verification and code generation for invariant diagrams in Isabelle.	J. Log. Algebraic Methods Program.	2015	DBLP DOI BibTeX RDF
16	Wenda Li, Grant Olney Passmore, Lawrence C. Paulson	A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL.	CoRR	2015	DBLP BibTeX RDF
16	Jørgen Villadsen, Alexander Birch Jensen, Anders Schlichtkrull	NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle.	CoRR	2015	DBLP BibTeX RDF
16	Christoph Benzmüller, Maximilian Claus, Nik Sultana	Systematic Verification of the Modal Logic Cube in Isabelle/HOL.	PxTP@CADE	2015	DBLP DOI BibTeX RDF
16	Lars Noschinski	A Graph Library for Isabelle.	Math. Comput. Sci.	2015	DBLP DOI BibTeX RDF
16	Frédéric Tuong, Burkhart Wolff	A Meta-Model for the Isabelle API.	Arch. Formal Proofs	2015	DBLP BibTeX RDF
16	René Thiemann, Akihisa Yamada 0002	Algebraic Numbers in Isabelle/HOL.	Arch. Formal Proofs	2015	DBLP BibTeX RDF
16	Lawrence C. Paulson	A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle.	J. Autom. Reason.	2015	DBLP DOI BibTeX RDF
16	Yongjian Li, Jun Pang 0001	Formalizing provable anonymity in Isabelle/HOL.	Formal Aspects Comput.	2015	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Jim Woodcock 0001	Mechanised Theory Engineering in Isabelle.	Dependable Software Systems Engineering	2015	DBLP DOI BibTeX RDF
16	Alexander Schimpf, Jan-Georg Smaus	Büchi Automata Optimisations Formalised in Isabelle/HOL.	ICLA	2015	DBLP DOI BibTeX RDF
16	Gergely Buday	Formalising the SECD machine with nominal Isabelle.	SAC	2015	DBLP DOI BibTeX RDF
16	Filip Maric, Predrag Janicic, Marko Malikovic	Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3.	CADE	2015	DBLP DOI BibTeX RDF
16	Declan Thompson	Formalisation vs. Understanding - A Case Study in Isabelle.	UCNC	2015	DBLP DOI BibTeX RDF
16	Fadoua Ghourabi, Kazuko Takahashi	Formalizing the Qualitative Superposition of Rectangles in Proof Assistant Isabelle/HOL.	ICAART (2)	2015	DBLP BibTeX RDF
16	David Déharbe, Stephan Merz	Software Component Design with the B Method - A Formalization in Isabelle/HOL.	FACS	2015	DBLP DOI BibTeX RDF
16	T. V. H. Prathamesh	Formalising Knot Theory in Isabelle/HOL.	ITP	2015	DBLP DOI BibTeX RDF
16	Andreas Lochbihler, Alexandra Maximova	Stream Fusion for Isabelle's Code Generator - Rough Diamond.	ITP	2015	DBLP DOI BibTeX RDF
16	Ondrej Kuncar, Andrei Popescu 0001	A Consistent Foundation for Isabelle/HOL.	ITP	2015	DBLP DOI BibTeX RDF
16	Christian Sternagel, René Thiemann	Deriving Comparators and Show Functions in Isabelle/HOL.	ITP	2015	DBLP DOI BibTeX RDF
16	Ondrej Kuncar	Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants.	CPP	2015	DBLP DOI BibTeX RDF
16	Manuel Eberl	A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL.	CPP	2015	DBLP DOI BibTeX RDF
16	Jesús Aransay, Jose Divasón	Generalizing a Mathematical Analysis Library in Isabelle/HOL.	NFM	2015	DBLP DOI BibTeX RDF
16	Fabian Immler	Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems.	ARCH@CPSWeek	2015	DBLP DOI BibTeX RDF
16	Victor Borges Ferreira Gomes	Algebraic principles for program correctness tools in Isabelle/HOL.		2015	RDF
16	Maria Spichkova	Stream processing components: Isabelle/HOL formalisation and case studies.	CoRR	2014	DBLP BibTeX RDF
16	Marco B. Caminati, Manfred Kerber, Christoph Lange 0002, Colin Rowat	Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?	CoRR	2014	DBLP BibTeX RDF
16	Lars Hupel	Interactive Simplifier Tracing and Debugging in Isabelle.	CoRR	2014	DBLP BibTeX RDF
16	Makarius Wenzel	System description: Isabelle/jEdit in 2014.	UITP	2014	DBLP DOI BibTeX RDF
16	David A. Cock	pGCL for Isabelle.	Arch. Formal Proofs	2014	DBLP BibTeX RDF
16	Christian Sternagel, René Thiemann	Haskell's Show-Class in Isabelle/HOL.	Arch. Formal Proofs	2014	DBLP BibTeX RDF
16	Mike Stannett, István Németi	Using Isabelle/HOL to Verify First-Order Relativity Theory.	J. Autom. Reason.	2014	DBLP DOI BibTeX RDF
16	György J. Simon, Genevieve B. Melton	A Gentle Introduction to Support Vector Machines in Biomedicine, Alexander Statnikov, Constantin F. Aliferis, Douglas P. Hardin, Isabelle Guyon. World Scientific (2013). Vols. 1(200 p.) and 2 (212 p.).	J. Biomed. Informatics	2014	DBLP DOI BibTeX RDF
16	Tobias Nipkow, Gerwin Klein	Concrete Semantics - With Isabelle/HOL		2014	DOI RDF
16	Alasdair Armstrong, Victor B. F. Gomes, Georg Struth	Algebras for Program Correctness in Isabelle/HOL.	RAMiCS	2014	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Frank Zeyda, Jim Woodcock 0001	Isabelle/UTP: A Mechanised Theory Engineering Framework.	UTP	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	David A. Cock	From Operational Models to Information Theory; Side Channels in pGCL with Isabelle.	ITP	2014	DBLP DOI BibTeX RDF
16	Daniel Matichuk, Makarius Wenzel, Toby C. Murray	An Isabelle Proof Method Language.	ITP	2014	DBLP DOI BibTeX RDF
16	Makarius Wenzel	Asynchronous User Interaction and Tool Integration in Isabelle/PIDE.	ITP	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	Marco B. Caminati, Manfred Kerber, Christoph Lange 0002, Colin Rowat	Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?	CICM	2014	DBLP DOI BibTeX RDF
16	Lars Hupel	Interactive Simplifier Tracing and Debugging in Isabelle.	CICM	2014	DBLP DOI BibTeX RDF
16	Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel	Certified HLints with Isabelle/HOLCF-Prelude.	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	Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel, Burkhart Wolff	The Circus Testing Theory Revisited in Isabelle/HOL.	ICFEM	2013	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Jim Woodcock 0001	Unifying Theories of Programming in Isabelle.	ICTAC Training School on Software Engineering	2013	DBLP DOI BibTeX RDF
16	Steffen Juilf Smolka, Jasmin Christian Blanchette	Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs.	PxTP@CADE	2013	DBLP DOI BibTeX RDF
16	Florian Kammüller, Yoney Kirsal Ever, Xiaochun Cheng	DNSsec in Isabelle - Replay Attack and Origin Authentication.	SMC	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	Andreas Lochbihler	Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable.	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	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	Alfio Martini	Programming Language Semantics with Isabelle/HOL.	WEIT	2013	DBLP DOI BibTeX RDF
16	Walther Neuper	Computer algebra implemented in Isabelle's function package under Lucas-interpretation - a case study.	CICM Workshops	2013	DBLP BibTeX RDF
16	Christoph Lüth, Martin Ring	A Web Interface for Isabelle: The Next Generation.	MKM/Calculemus/DML	2013	DBLP DOI BibTeX RDF
16	Mike Stannett, István Németi	Using Isabelle to verify special relativity, with application to hypercomputation theory	CoRR	2012	DBLP BibTeX RDF
16	Christian Urban, Cezary Kaliszyk	General Bindings and Alpha-Equivalence in Nominal Isabelle	Log. Methods Comput. Sci.	2012	DBLP DOI BibTeX RDF
16	Makarius Wenzel	Isabelle/jEdit --- a Prover IDE within the PIDE framework	CoRR	2012	DBLP BibTeX RDF
16	Christian Sternagel	Getting Started with Isabelle/jEdit	CoRR	2012	DBLP BibTeX RDF
16	David A. Cock	Verifying Probabilistic Correctness in Isabelle with pGCL	SSV	2012	DBLP DOI BibTeX RDF
16	Abderrahmane Feliachi, Burkhart Wolff, Marie-Claude Gaudel	Isabelle/Circus.	Arch. Formal Proofs	2012	DBLP BibTeX RDF
16	Jesper Bengtson	Psi-calculi in Isabelle.	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	Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff	Isabelle/Circus: A Process Specification and Verification Environment.	VSTTE	2012	DBLP DOI BibTeX RDF
16	Lukas Bulwahn	Smart Testing of Functional Programs in Isabelle.	LPAR	2012	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, Andrei Popescu 0001, Daniel Wand, Christoph Weidenbach	More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification.	ITP	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	Lukas Bulwahn	The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof.	CPP	2012	DBLP DOI BibTeX RDF
16	Makarius Wenzel	Isabelle/jEdit - A Prover IDE within the PIDE Framework.	AISC/MKM/Calculemus	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	Makarius Wenzel, Burkhart Wolff	Isabelle/PIDE as Platform for Educational Tools	ThEdu	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	Walter Guttmann, Georg Struth, Tjark Weber	Automating Algebraic Methods in Isabelle.	ICFEM	2011	DBLP DOI BibTeX RDF
16	Cezary Kaliszyk, Christian Urban	Quotients revisited for Isabelle/HOL.	SAC	2011	DBLP DOI BibTeX RDF
16	Christian Urban, Cezary Kaliszyk	General Bindings and Alpha-Equivalence in Nominal Isabelle.	ESOP	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	Alexander Krauss 0001, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl	Termination of Isabelle Functions via Termination of Rewriting.	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	Cezary Kaliszyk, Henk Barendregt	Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem.	CPP	2011	DBLP DOI BibTeX RDF
16	Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow	Automatic Proof and Disproof in Isabelle/HOL.	FroCoS	2011	DBLP DOI BibTeX RDF
16	Stefan Berghofer	Verification of Dependable Software using SPARK and Isabelle.	SSV	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	Makarius Wenzel	Isabelle as Document-Oriented Proof Assistant.	Calculemus/MKM	2011	DBLP DOI BibTeX RDF
16	Laura I. Meikle, Jacques D. Fleuriot	Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover's Palette.	UITP	2010	DBLP DOI BibTeX RDF
16	Ludovic Henrio, Muhammad Uzair Khan	Asynchronous Components with Futures: Semantics and Proofs in Isabelle/HOL.	FESCA@ETAPS	2010	DBLP DOI BibTeX RDF