Search results for "isabelle"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
27	Jesper Bengtson, Joachim Parrow	Psi-calculi in Isabelle.	TPHOLs	2009	DBLP DOI BibTeX RDF
27	Jinshuang Wang, Huabing Yang, Xingyuan Zhang	Liveness Reasoning with Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF	Liveness Proof, Inductive Protocol Verification, Parametric Fairness, Probabilistic Model
27	Christian Urban	Nominal Techniques in Isabelle/HOL.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Nominal logic work, Lambda-calculus, Theorem provers
27	Laura I. Meikle, Jacques D. Fleuriot	Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B.	CAV	2008	DBLP DOI BibTeX RDF
27	Lukas Bulwahn, Alexander Krauss 0001, Florian Haftmann, Levent Erkök, John Matthews	Imperative Functional Programming with Isabelle/HOL.	TPHOLs	2008	DBLP DOI BibTeX RDF
27	Daniel Wasserrab, Andreas Lochbihler	Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL.	TPHOLs	2008	DBLP DOI BibTeX RDF
27	Lawrence C. Paulson	The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF.	CiE	2008	DBLP DOI BibTeX RDF
27	Laura I. Meikle, Jacques D. Fleuriot	Combining Isabelle and QEPCAD-B in the Prover's Palette.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
27	Hamdi Yahyaoui, Mourad Debbabi, Nadia Tawbi	A Denotational Semantic Model for Validating JVML/CLDC Optimizations under Isabelle/HOL.	QSIC	2007	DBLP DOI BibTeX RDF
27	Christian Urban, Stefan Berghofer	A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF	Lambda-calculus, proof assistants, nominal logic, primitive recursion
27	Makarius Wenzel	Structured Induction Proofs in Isabelle/Isar.	MKM	2006	DBLP DOI BibTeX RDF
27	Brian Huffman, John Matthews, Peter White	Axiomatic Constructor Classes in Isabelle/HOLCF.	TPHOLs	2005	DBLP DOI BibTeX RDF
27	Christian Urban, Christine Tasson	Nominal Techniques in Isabelle/HOL.	CADE	2005	DBLP DOI BibTeX RDF	theorem-assistants, Lambda-calculus, nominal logic, structural induction
27	Norbert Schirmer	A Verification Environment for Sequential Imperative Programs in Isabelle/HOL.	LPAR	2004	DBLP DOI BibTeX RDF
27	Baris Sertkaya, Halit Oguztüzün	Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL.	ISCIS	2004	DBLP DOI BibTeX RDF
27	Jeremy Avigad, Kevin Donnelly	Formalizing O Notation in Isabelle/HOL.	IJCAR	2004	DBLP DOI BibTeX RDF
27	Stefan Berghofer, Tobias Nipkow	Random Testing in Isabelle/HOL.	SEFM	2004	DBLP DOI BibTeX RDF
27	Wolfram Kahl	Calculational Relation-Algebraic Proofs in Isabelle/Isar.	RelMiCS	2003	DBLP DOI BibTeX RDF
27	Leonor Prensa Nieto	The Rely-Guarantee Method in Isabelle/HOL.	ESOP	2003	DBLP DOI BibTeX RDF
27	Stefan Berghofer	A Constructive Proof of Higman's Lemma in Isabelle.	TYPES	2003	DBLP DOI BibTeX RDF
27	Clemens Ballarin	Locales and Locale Expressions in Isabelle/Isar.	TYPES	2003	DBLP DOI BibTeX RDF
27	Yasuhiko Minamide, Koji Okuma	Verifying CPS transformations in Isabelle/HOL.	MERLIN	2003	DBLP DOI BibTeX RDF	program transformation, theorem proving, correctness proofs
27	Lucas Dixon, Jacques D. Fleuriot	IsaPlanner: A Prototype Proof Planner in Isabelle.	CADE	2003	DBLP DOI BibTeX RDF
27	Martin Strecker	Investigating Type-Certifying Compilation with Isabelle.	LPAR	2002	DBLP DOI BibTeX RDF
27	Gertrud Bauer, Tobias Nipkow	The 5 Colour Theorem in Isabelle/Isar.	TPHOLs	2002	DBLP DOI BibTeX RDF
27	Martin Strecker	Formal Verification of a Java Compiler in Isabelle.	CADE	2002	DBLP DOI BibTeX RDF
27	David Hemer, Ian J. Hayes, Paul A. Strooper	Refinement Calculus for Logic Programming in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF
27	Stephan Merz	Weak Alternating Automata in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
27	Jacques D. Fleuriot	On the Mechanization of Real Analysis in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
27	Florian Kammüller, Markus Wenzel 0001, Lawrence C. Paulson	Locales - A Sectioning Concept for Isabelle.	TPHOLs	1999	DBLP DOI BibTeX RDF
27	Jacques D. Fleuriot, Lawrence C. Paulson	Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle.	Automated Deduction in Geometry	1998	DBLP DOI BibTeX RDF
27	Jeremy E. Dawson, Rajeev Goré	A Mechanisation of Classical Modal Tense Logics Using Isabelle.	Australian Joint Conference on Artificial Intelligence	1998	DBLP DOI BibTeX RDF	logics for knowledge and belief, display logic, sequent calculus, automated deduction, hybrid logics, tense logic
27	Sten Agerholm, Jacob Frost	An Isabelle-Based Theorem Prover for VDM-SL.	TPHOLs	1997	DBLP DOI BibTeX RDF
27	Martin Simons 0001	Proof Presentation for Isabelle.	TPHOLs	1997	DBLP DOI BibTeX RDF
27	Olaf Müller, Tobias Nipkow	Traces of I/O-Automata in Isabelle/HOLCF.	TAPSOFT	1997	DBLP DOI BibTeX RDF
27	Seán Matthews	Implementing FS0 in Isabelle: Adding Structure at the Metalevel.	DISCO	1996	DBLP DOI BibTeX RDF
21	Jasmin Christian Blanchette	Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Interactive theorem provers, Huffman coding, Higher-order logic
21	Javier de Dios, Ricardo Peña-Marí	Formal Certification of a Resource-Aware Language Implementation.	TPHOLs	2009	DBLP DOI BibTeX RDF	memory management, functional languages, compiler verification
21	Stefan Berghofer, Markus Reiter	Formalizing the Logic-Automaton Connection.	TPHOLs	2009	DBLP DOI BibTeX RDF
21	Jeremy E. Dawson, Alwen Tiu	Formalising Observer Theory for Environment-Sensitive Bisimulation.	TPHOLs	2009	DBLP DOI BibTeX RDF
21	Rafal Kolanski, Gerwin Klein	Types, Maps and Separation Logic.	TPHOLs	2009	DBLP DOI BibTeX RDF
21	Christoph Lüth, Dennis Walter	Certifiable Specification and Verification of C Programs.	FM	2009	DBLP DOI BibTeX RDF
21	Levent Erkök, John Matthews	Pragmatic equivalence and safety checking in Cryptol.	PLPV	2009	DBLP DOI BibTeX RDF	sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking
21	Klaus Aehlig, Florian Haftmann, Tobias Nipkow	A Compiled Implementation of Normalization by Evaluation.	TPHOLs	2008	DBLP DOI BibTeX RDF
21	Rok Strnisa, Peter Sewell, Matthew J. Parkinson	The java module system: core design and semantic definition.	OOPSLA	2007	DBLP DOI BibTeX RDF	LJAM, superpackage, java, module, JAM
21	Christoph Sprenger 0001, David A. Basin	A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols.	TPHOLs	2007	DBLP DOI BibTeX RDF
21	Jeremy E. Dawson	Formalising Generalised Substitutions.	TPHOLs	2007	DBLP DOI BibTeX RDF	general correctness, generalised substitution
21	Jesper Bengtson, Joachim Parrow	Formalising the pi-Calculus Using Nominal Logic.	FoSSaCS	2007	DBLP DOI BibTeX RDF
21	Amine Chaieb, Makarius Wenzel	Context Aware Calculation and Deduction.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
21	Viktor Kuncak, Martin C. Rinard	An overview of the Jahob analysis system: project goals and current status.	IPDPS	2006	DBLP DOI BibTeX RDF
21	Tom Ridge, James Margetson	A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.	TPHOLs	2005	DBLP DOI BibTeX RDF
21	Laura I. Meikle, Jacques D. Fleuriot	Mechanical Theorem Proving in Computational Geometry.	Automated Deduction in Geometry	2004	DBLP DOI BibTeX RDF
21	Martin Wildmoser, Tobias Nipkow	Certifying Machine Code Safety: Shallow Versus Deep Embedding.	TPHOLs	2004	DBLP DOI BibTeX RDF
21	Morten P. Lindegaard, Anne E. Haxthausen	Proof Support for RAISE by a Reuse Approach Based on Institutions.	AMAST	2004	DBLP DOI BibTeX RDF	proof support, Institutions, algebraic semantics, HOL, RSL
21	Michael Drouineaud, Maksym Bortin, Paolo Torrini, Karsten Sohr	A First Step Towards Formal Verification of Security Policy Properties for RBAC.	QSIC	2004	DBLP DOI BibTeX RDF
21	Jeremy E. Dawson, Rajeev Goré	Formalised Cut Admissibility for Display Logic.	TPHOLs	2002	DBLP DOI BibTeX RDF
21	Marieke Huisman	Verification of Java's AbstractCollection Class: A Case Study.	MPC	2002	DBLP DOI BibTeX RDF
21	Lawrence C. Paulson	The Reflection Theorem: A Study in Meta-theoretic Reasoning.	CADE	2002	DBLP DOI BibTeX RDF
21	David von Oheimb, Volkmar Lotz	Formal Security Analysis with Interacting State Machines.	ESORICS	2002	DBLP DOI BibTeX RDF
21	Steffen Helke, Florian Kammüller	Representing Hierarchical Automata in Interactive Theorem Provers.	TPHOLs	2001	DBLP DOI BibTeX RDF
21	Jacques D. Fleuriot	Nonstandard Geometric Proofs.	Automated Deduction in Geometry	2000	DBLP DOI BibTeX RDF
21	Bernhard Reus, Tatjana Hein	Towards a Machine-Checked Java Specification Book.	TPHOLs	2000	DBLP DOI BibTeX RDF
21	Christine Röckl, Javier Esparza	Proof-Checking Protocols Using Bisimulations.	CONCUR	1999	DBLP DOI BibTeX RDF
21	Lawrence C. Paulson	Inductive Analysis of the Internet Protocol TLS (Position Paper).	Security Protocols Workshop	1998	DBLP DOI BibTeX RDF
21	Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant	Proof Tactics for a Theory of State Machines in a Graphical Environment.	CADE	1997	DBLP DOI BibTeX RDF
21	David R. Lester, Sava Mintchev	Towards Machine-Checked Compiler Correctness for Higher-order Pure Functional Languages.	CSL	1994	DBLP DOI BibTeX RDF	Congruence Proof, Lambda Calculus, Denotational Semantics, Theorem Prover, Compiler Correctness
20	Andrei Popescu 0001, Elsa L. Gunter, Christopher J. Osborn	Strong Normalization for System F by HOAS on Top of FOAS.	LICS	2010	DBLP DOI BibTeX RDF	Higher-Order Abstract Syntax, Isabelle/HOL, System F
20	Ihor Kuz, Gerwin Klein, Corey Lewis, Adam Walker	capDL: a language for describing capability-based systems.	ApSys	2010	DBLP DOI BibTeX RDF	SEL4, capability distribution, capabilities, security analysis, isabelle
20	Patrick Schaller, Benedikt Schmidt 0002, David A. Basin, Srdjan Capkun	Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks.	CSF	2009	DBLP DOI BibTeX RDF	Wireless Network Protocols, Security Protocols, Isabelle/HOL, Formal Security Model
20	Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood	seL4: formal verification of an OS kernel.	SOSP	2009	DBLP DOI BibTeX RDF	l4, sel4, microkernel, isabelle/hol
20	Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty	Running the manual: an approach to high-assurance microkernel development.	Haskell	2006	DBLP DOI BibTeX RDF	formalisation, verification, operating systems, rapid prototyping, Haskell, monads, executable specification, Isabelle/HOL
16	Jonathan Julián Huerta y Munive, Simon Foster 0001, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman	Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL.	CoRR	2024	DBLP DOI BibTeX RDF
16	Julian Parsert	Linear Programming in Isabelle/HOL.	CoRR	2024	DBLP DOI BibTeX RDF
16	Terru Stübinger, Lars Hupel	Go Code Generation for Isabelle.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
16	Xavier Parent, Christoph Benzmüller	Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset).	Arch. Formal Proofs	2024	DBLP BibTeX RDF
16	Mnacho Echenim, Mehdi Mhalla	A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL.	J. Autom. Reason.	2024	DBLP DOI BibTeX RDF
16	Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds 0001, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli	IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.	TACAS (1)	2024	DBLP DOI BibTeX RDF
16	Sohaib Soualah, Mohamed Khalgui, Allaoua Chaoui	Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL.	AINA (2)	2024	DBLP DOI BibTeX RDF
16	Conrad Watt, Maja Trela, Peter Lammich, Florian Märkl	WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly.	Proc. ACM Program. Lang.	2023	DBLP DOI BibTeX RDF
16	Andreas V. Hess, Sebastian Alexander Mödersheim, Achim D. Brucker	Stateful Protocol Composition in Isabelle/HOL.	ACM Trans. Priv. Secur.	2023	DBLP DOI BibTeX RDF
16	Florian Kammüller, Dimpy Satija	Explanation of Student Attendance AI Prediction with the Isabelle Infrastructure Framework.	Inf.	2023	DBLP DOI BibTeX RDF
16	Jonas Bayer, Aleksey Gonus, Christoph Benzmüller, Dana S. Scott	Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation.	CoRR	2023	DBLP DOI BibTeX RDF
16	Florian Kammüller	Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security.	CoRR	2023	DBLP DOI BibTeX RDF
16	Ata Keskin	A Formalization of Martingales in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
16	Chelsea Edmonds, Lawrence C. Paulson	Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
16	Leo Freitas	Topologically sorting VDM-SL definitions for Isabelle/HOL translation.	CoRR	2023	DBLP DOI BibTeX RDF
16	Simon Foster 0001, Burkhart Wolff	Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
16	Lex Bailey, Jim Woodcock 0001, Simon Foster 0001, Roberto Metere	Checking and Automating Confidentiality Theory in Isabelle/UTP.	CoRR	2023	DBLP DOI BibTeX RDF
16	Marco B. Caminati	Isabelle Formalisation of Original Representation Theorems.	CoRR	2023	DBLP DOI BibTeX RDF
16	Terru Stübinger, Lars Hupel	Extending Isabelle/HOL's Code Generator with support for the Go programming language.	CoRR	2023	DBLP DOI BibTeX RDF
16	Stepán Starosta	Infinite Words and Morphic Languages Formalized in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
16	Leo Freitas, Peter Gorm Larsen	VDM recursive functions in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
16	Mnacho Echenim, Mehdi Mhalla	A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
16	Kevin Kappelmann	Unification Utilities for Isabelle/ML.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
16	Simon Roßkopf, Tobias Nipkow	A Formalization and Proof Checker for Isabelle's Metalogic.	J. Autom. Reason.	2023	DBLP DOI BibTeX RDF
16	Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson	Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL.	J. Autom. Reason.	2023	DBLP DOI BibTeX RDF
16	Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot	Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL.	J. Autom. Reason.	2023	DBLP DOI BibTeX RDF
16	Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen	A sequent calculus for first-order logic formalized in Isabelle/HOL.	J. Log. Comput.	2023	DBLP DOI BibTeX RDF
16	Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001	Program logic for higher-order probabilistic programs in Isabelle/HOL.	Sci. Comput. Program.	2023	DBLP DOI BibTeX RDF
16	Pasquale Noce	Formal Verification of Cryptographic Protocols with Isabelle/HOL.	Handb. Formal Anal. Verification Cryptogr.	2023	DBLP DOI BibTeX RDF