Search results for "Isabelle/HOL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
186	Steven Obua, Sebastian Skalberg	Importing HOL into Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF
128	Sean McLaughlin	An Interpretation of Isabelle/HOL in HOL Light.	IJCAR	2006	DBLP DOI BibTeX RDF
103	Graeme Smith 0001, Florian Kammüller, Thomas Santen	Encoding Object-Z in Isabelle/HOL.	ZB	2002	DBLP DOI BibTeX RDF	reference semantics, Object-Z, higher-order logic, Isabelle
93	Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow	The Isabelle Framework.	TPHOLs	2008	DBLP DOI BibTeX RDF
92	Alexander Schimpf, Stephan Merz, Jan-Georg Smaus	Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
92	Florian Kammüller, Jeff W. Sanders	Idempotent Relations in Isabelle/HOL.	ICTAC	2004	DBLP DOI BibTeX RDF
91	Markus Kaiser 0002, Ralf Lämmel	An Isabelle/HOL-based model of stratego-like traversal strategies.	PPDP	2009	DBLP DOI BibTeX RDF	generic functional programming, traversal strategies, domain specific languages, rewriting, isabelle/hol, software transformation, stratego
83	Haykal Tej, Burkhart Wolff	A Corrected Failure Divergence Model for CSP in Isabelle/HOL.	FME	1997	DBLP DOI BibTeX RDF
82	Thomas Santen	A Theory of Structured Model-Based Specifications in Isabelle/HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
80	Sabine Glesner, Jan Olaf Blech	Coalgebraic Semantics for Component Systems.	Architecting Systems with Trustworthy Components	2004	DBLP DOI BibTeX RDF	verification, semantics, Components, Isabelle/HOL, coinduction, component interaction
80	David von Oheimb, Tobias Nipkow	Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited.	FME	2002	DBLP DOI BibTeX RDF	Java, Hoare logic, side effects, dynamic binding, Isabelle/HOL, auxiliary variables
80	David von Oheimb	Hoare Logic for Mutual Recursion and Local Variables.	FSTTCS	1999	DBLP DOI BibTeX RDF	axiomaticsemantics, relative completeness, local variables, call-by-value parameters, soundness, Hoare logic, Isabelle/HOL, mutual recursion
79	Achim D. Brucker, Burkhart Wolff	Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing.	TAP	2007	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation
73	Yue Tang, Jin Song Dong, Jing Sun 0002, Brendan P. Mahony	Reasoning about Semantic Web in Isabelle/HOL.	APSEC	2004	DBLP DOI BibTeX RDF
72	Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner	Formal Verification of Dead Code Elimination in Isabelle/HOL.	SEFM	2005	DBLP DOI BibTeX RDF
72	Stefan Berghofer	Extracting a Normalization Algorithm in Isabelle/HOL.	TYPES	2004	DBLP DOI BibTeX RDF
72	Christine Röckl, Daniel Hirschkoff, Stefan Berghofer	Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts.	FoSSaCS	2001	DBLP DOI BibTeX RDF
72	Cornelia Pusch	Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL.	TACAS	1999	DBLP DOI BibTeX RDF
64	Albert Rizaldi	Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL (Formale Spezifikation, Erfüllbarkeitsanalyse, und formale Verifikation von autonomen Fahrzeugen in Isabelle/HOL) (PDF / PS)		2020	RDF
63	Andreas Lochbihler	Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
63	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
63	Simon J. Gay	A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF	semantics, Types, pi calculus, automatic theorem proving
63	Leonor Prensa Nieto, Javier Esparza	Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL.	MFCS	2000	DBLP DOI BibTeX RDF
63	Pierre Chartier	Formalisation of B in Isabelle/HOL.	B	1998	DBLP DOI BibTeX RDF
63	Tobias Nipkow	More Church-Rosser Proofs (in Isabelle/HOL).	CADE	1996	DBLP DOI BibTeX RDF
62	Damián Barsotti, Leonor Prensa Nieto, Alwen Tiu	Verification of clock synchronization algorithms: experiments on a combination of deductive tools.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Combination of deductive tools, Verification, Theorem proving, Clock synchronization
62	Christian Urban	Nominal Techniques in Isabelle/HOL.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Nominal logic work, Lambda-calculus, Theorem provers
62	Jacques D. Fleuriot	On the Mechanization of Real Analysis in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
60	Dirk Leinenbach, Wolfgang J. Paul, Elena Petrova	Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes.	SEFM	2005	DBLP DOI BibTeX RDF
60	Matthias Daum 0001, Jan Dörrenbächer, Burkhart Wolff	Proving Fairness and Implementation Correctness of a Microkernel Scheduler.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL
60	Gerwin Klein, Philip Derrin, Kevin Elphinstone	Experience report: seL4: formally verifying a high-performance microkernel.	ICFP	2009	DBLP DOI BibTeX RDF	seL4, haskell, microkernel, Isabelle/HOL
60	Nik Sultana, Simon J. Thompson	Mechanical verification of refactorings.	PEPM	2008	DBLP DOI BibTeX RDF	refactoring, Isabelle/HOL
60	Sabine Glesner	Finite Integer Computations: An Algebraic Foundation for Their Correctness.	Formal Aspects Comput.	2006	DBLP DOI BibTeX RDF	Additional Keywords finite integer and residue class arithmetic, changing representation sizes, Java Card bytecode optimization, constant folding, Java and C arithmetic, formal verification, inconsistency, Java Card, Isabelle/HOL
60	David von Oheimb, Volkmar Lotz, Georg Walter	Analyzing SLE 88 memory management security using Interacting State Machines.	Int. J. Inf. Sec.	2005	DBLP DOI BibTeX RDF	Security, Smart cards, Memory management, Formal analysis, Isabelle/HOL
60	S. J. Ambler, Roy L. Crole, Alberto Momigliano	A definitional approach to primitivexs recursion over higher order abstract syntax.	MERLIN	2003	DBLP DOI BibTeX RDF	Isabelle HOL, topos theory, ?-calculus, higher order abstract syntax, primitive recursion, initial algebras
60	Lawrence C. Paulson	Mechanized proofs for a recursive authentication protocol.	CSFW	1997	DBLP DOI BibTeX RDF	mechanized proofs, recursive authentication protocol, inductive approach, message nesting, basic security theorem, adjacent pairs, honest agents, protocol complexity, agents, protocols, specification, symmetry, mutual authentication, Isabelle/HOL, session keys
59	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
52	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
52	Lukas Bulwahn, Alexander Krauss 0001, Florian Haftmann, Levent Erkök, John Matthews	Imperative Functional Programming with Isabelle/HOL.	TPHOLs	2008	DBLP DOI BibTeX RDF
52	Daniel Wasserrab, Andreas Lochbihler	Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL.	TPHOLs	2008	DBLP DOI BibTeX RDF
52	William Billingsley, Peter Robinson 0001	Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Intelligent book, MathsTiles, Isabelle
52	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
52	Christian Urban, Christine Tasson	Nominal Techniques in Isabelle/HOL.	CADE	2005	DBLP DOI BibTeX RDF	theorem-assistants, Lambda-calculus, nominal logic, structural induction
52	Norbert Schirmer	A Verification Environment for Sequential Imperative Programs in Isabelle/HOL.	LPAR	2004	DBLP DOI BibTeX RDF
52	Baris Sertkaya, Halit Oguztüzün	Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL.	ISCIS	2004	DBLP DOI BibTeX RDF
52	Jeremy Avigad, Kevin Donnelly	Formalizing O Notation in Isabelle/HOL.	IJCAR	2004	DBLP DOI BibTeX RDF
52	Leonor Prensa Nieto	The Rely-Guarantee Method in Isabelle/HOL.	ESOP	2003	DBLP DOI BibTeX RDF
52	Yasuhiko Minamide, Koji Okuma	Verifying CPS transformations in Isabelle/HOL.	MERLIN	2003	DBLP DOI BibTeX RDF	program transformation, theorem proving, correctness proofs
52	David Hemer, Ian J. Hayes, Paul A. Strooper	Refinement Calculus for Logic Programming in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF
52	Stephan Merz	Weak Alternating Automata in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
51	Markus Wenzel 0001, Lawrence C. Paulson	Isabelle/Isar.	The Seventeen Provers of the World	2006	DBLP DOI BibTeX RDF
51	Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.	TACAS	2006	DBLP DOI BibTeX RDF
51	Steffen Helke, Florian Kammüller	Structure Preserving Data Abstractions for Statecharts.	FORTE	2005	DBLP DOI BibTeX RDF
50	Martin Wildmoser, Tobias Nipkow	Certifying Machine Code Safety: Shallow Versus Deep Embedding.	TPHOLs	2004	DBLP DOI BibTeX RDF
48	Hao Xu, Yongwang Zhao	Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving.	Internetware	2023	DBLP DOI BibTeX RDF
48	Achim D. Brucker	Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
48	Diego Marmsoler, Achim D. Brucker	Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
47	Xavier Parent, Christoph Benzmüller	Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset).	Arch. Formal Proofs	2024	DBLP BibTeX RDF
47	Ondrej Kuncar, Andrei Popescu 0001	Safety and conservativity of definitions in HOL and Isabelle/HOL.	Proc. ACM Program. Lang.	2018	DBLP DOI BibTeX RDF
47	Dina Taiwé Kolyang	HOL-Z, an integrated formal support environment for Z in Isabelle/HOL.		1999	RDF
41	René Thiemann, Christian Sternagel	Certification of Termination Proofs Using CeTA.	TPHOLs	2009	DBLP DOI BibTeX RDF
41	Stefan Berghofer	Program Extraction in Simply-Typed Higher Order Logic.	TYPES	2002	DBLP DOI BibTeX RDF
40	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
40	Jeremy E. Dawson, Alwen Tiu	Formalising Observer Theory for Environment-Sensitive Bisimulation.	TPHOLs	2009	DBLP DOI BibTeX RDF
40	Rafal Kolanski, Gerwin Klein	Types, Maps and Separation Logic.	TPHOLs	2009	DBLP DOI BibTeX RDF
40	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
40	Christoph Sprenger 0001, David A. Basin	A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols.	TPHOLs	2007	DBLP DOI BibTeX RDF
40	Tom Ridge, James Margetson	A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.	TPHOLs	2005	DBLP DOI BibTeX RDF
40	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
40	Jeremy E. Dawson, Rajeev Goré	Formalised Cut Admissibility for Display Logic.	TPHOLs	2002	DBLP DOI BibTeX RDF
40	Christine Röckl, Javier Esparza	Proof-Checking Protocols Using Bisimulations.	CONCUR	1999	DBLP DOI BibTeX RDF
40	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
40	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
40	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
40	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
39	Achim D. Brucker, Burkhart Wolff	hol-TestGen.	FASE	2009	DBLP DOI BibTeX RDF	symbolic test-case generations, theorem proving, black box testing, white box testing, interactive testing
39	Ludovic Henrio, Florian Kammüller	A Mechanized Model of the Theory of Objects.	FMOODS	2007	DBLP DOI BibTeX RDF
39	Achim D. Brucker, Burkhart Wolff	Interactive Testing with HOL-TestGen.	FATES	2005	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, black box testing, white box testing, interactive testing
39	Thomas Santen	Isomorphisms - A Link Between the Shallow and the Deep.	TPHOLs	1999	DBLP DOI BibTeX RDF
32	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
32	Julian Parsert	Linear Programming in Isabelle/HOL.	CoRR	2024	DBLP DOI BibTeX RDF
32	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
32	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
32	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
32	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
32	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
32	Ata Keskin	A Formalization of Martingales in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
32	Chelsea Edmonds, Lawrence C. Paulson	Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
32	Leo Freitas	Topologically sorting VDM-SL definitions for Isabelle/HOL translation.	CoRR	2023	DBLP DOI BibTeX RDF
32	Simon Foster 0001, Burkhart Wolff	Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
32	Terru Stübinger, Lars Hupel	Extending Isabelle/HOL's Code Generator with support for the Go programming language.	CoRR	2023	DBLP DOI BibTeX RDF
32	Stepán Starosta	Infinite Words and Morphic Languages Formalized in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
32	Leo Freitas, Peter Gorm Larsen	VDM recursive functions in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
32	Mnacho Echenim, Mehdi Mhalla	A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL.	CoRR	2023	DBLP DOI BibTeX RDF
32	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
32	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
32	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
32	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
32	Pasquale Noce	Formal Verification of Cryptographic Protocols with Isabelle/HOL.	Handb. Formal Anal. Verification Cryptogr.	2023	DBLP DOI BibTeX RDF
32	Achim D. Brucker, Amy Stell	Verifying Feedforward Neural Networks for Classification in Isabelle/HOL.	FM	2023	DBLP DOI BibTeX RDF