Search results for "Isabelle/HOL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Markus Kaiser, 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
2	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
2	Andreas Lochbihler	Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
2	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
2	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
2	Matthias Daum, Jan Dörrenbächer, Burkhart Wolff	Proving Fairness and Implementation Correctness of a Microkernel Scheduler.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL
2	Christian Urban	Nominal Techniques in Isabelle/HOL.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Nominal logic work, Lambda-calculus, Theorem provers
2	Daniel Wasserrab, Andreas Lochbihler	Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL.	TPHOLs	2008	DBLP DOI BibTeX RDF
2	Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews	Imperative Functional Programming with Isabelle/HOL.	TPHOLs	2008	DBLP DOI BibTeX RDF
2	Nik Sultana, Simon J. Thompson	Mechanical verification of refactorings.	PEPM	2008	DBLP DOI BibTeX RDF	refactoring, Isabelle/HOL
2	William Billingsley, Peter Robinson	Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Intelligent book, MathsTiles, Isabelle
2	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
2	Steven Obua, Sebastian Skalberg	Importing HOL into Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF
2	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
2	Sean McLaughlin	An Interpretation of Isabelle/HOL in HOL Light.	IJCAR	2006	DBLP DOI BibTeX RDF
2	Sabine Glesner	Finite Integer Computations: An Algebraic Foundation for Their Correctness.	Formal Asp. 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
2	Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner	Formal Verification of Dead Code Elimination in Isabelle/HOL.	SEFM	2005	DBLP DOI BibTeX RDF
2	Christian Urban, Christine Tasson	Nominal Techniques in Isabelle/HOL.	CADE	2005	DBLP DOI BibTeX RDF	theorem-assistants, Lambda-calculus, nominal logic, structural induction
2	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
2	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
2	Yue Tang, Jin Song Dong, Jing Sun 0002, Brendan P. Mahony	Reasoning about Semantic Web in Isabelle/HOL.	APSEC	2004	DBLP DOI BibTeX RDF
2	Jeremy Avigad, Kevin Donnelly	Formalizing O Notation in Isabelle/HOL.	IJCAR	2004	DBLP DOI BibTeX RDF
2	Norbert Schirmer	A Verification Environment for Sequential Imperative Programs in Isabelle/HOL.	LPAR	2004	DBLP DOI BibTeX RDF
2	Florian Kammüller, Jeff W. Sanders	Idempotent Relations in Isabelle/HOL.	ICTAC	2004	DBLP DOI BibTeX RDF
2	Stefan Berghofer	Extracting a Normalization Algorithm in Isabelle/HOL.	TYPES	2004	DBLP DOI BibTeX RDF
2	Baris Sertkaya, Halit Oguztüzün	Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL.	ISCIS	2004	DBLP DOI BibTeX RDF
2	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
2	Yasuhiko Minamide, Koji Okuma	Verifying CPS transformations in Isabelle/HOL.	MERLIN	2003	DBLP DOI BibTeX RDF	program transformation, theorem proving, correctness proofs
2	Leonor Prensa Nieto	The Rely-Guarantee Method in Isabelle/HOL.	ESOP	2003	DBLP DOI BibTeX RDF
2	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
2	Graeme Smith, 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
2	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
2	David Hemer, Ian J. Hayes, Paul A. Strooper	Refinement Calculus for Logic Programming in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF
2	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
2	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
2	Leonor Prensa Nieto, Javier Esparza	Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL.	MFCS	2000	DBLP DOI BibTeX RDF
2	Stephan Merz	Weak Alternating Automata in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
2	Jacques D. Fleuriot	On the Mechanization of Real Analysis in Isabelle/HOL.	TPHOLs	2000	DBLP DOI BibTeX RDF
2	Cornelia Pusch	Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL.	TACAS	1999	DBLP DOI BibTeX RDF
2	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
2	Pierre Chartier	Formalisation of B in Isabelle/HOL.	B	1998	DBLP DOI BibTeX RDF
2	Haykal Tej, Burkhart Wolff	A Corrected Failure Divergence Model for CSP in Isabelle/HOL.	FME	1997	DBLP DOI BibTeX RDF
2	Thomas Santen	A Theory of Structured Model-Based Specifications in Isabelle/HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
2	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
2	Tobias Nipkow	More Church-Rosser Proofs (in Isabelle/HOL).	CADE	1996	DBLP DOI BibTeX RDF
1	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
1	Gudmund Grov, Stephan Merz	A Definitional Encoding of TLA* in Isabelle/HOL.	Archive of Formal Proofs	2011	DBLP BibTeX RDF
1	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
1	Cezary Kaliszyk, Christian Urban	Quotients revisited for Isabelle/HOL.	SAC	2011	DBLP DOI BibTeX RDF
1	Simon Foster, Georg Struth, Tjark Weber	Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial).	RAMICS	2011	DBLP DOI BibTeX RDF
1	Johannes Hölzl, Armin Heller	Three Chapters of Measure Theory in Isabelle/HOL.	ITP	2011	DBLP DOI BibTeX RDF
1	Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow	Automatic Proof and Disproof in Isabelle/HOL.	FroCos	2011	DBLP DOI BibTeX RDF
1	Filip Maric	Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL.	Theor. Comput. Sci.	2010	DBLP DOI BibTeX RDF
1	Ludovic Henrio, Muhammad Uzair Khan	Asynchronous Components with Futures: Semantics and Proofs in Isabelle/HOL.	Electr. Notes Theor. Comput. Sci.	2010	DBLP DOI BibTeX RDF
1	Jacques D. Fleuriot	Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL.	Automated Deduction in Geometry	2010	DBLP DOI BibTeX RDF
1	Douglas J. Howe	Higher-Order Abstract Syntax in Isabelle/HOL.	ITP	2010	DBLP DOI BibTeX RDF
1	Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff	Unifying Theories in Isabelle/HOL.	UTP	2010	DBLP DOI BibTeX RDF
1	Maksym Bortin, Christoph Lüth	Structured Formal Development with Quotient Types in Isabelle/HOL.	AISC/MKM/Calculemus	2010	DBLP DOI BibTeX RDF
1	Andrei Popescu, 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
1	Bart Kastermans	An Example of a Cofinitary Group in Isabelle/HOL.	Archive of Formal Proofs	2009	DBLP BibTeX RDF
1	Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu	Theory support for weak higher order abstract syntax in Isabelle/HOL.	LFMTP	2009	DBLP DOI BibTeX RDF
1	Christian Doczkal, Jan Schwinghammer	Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal.	LFMTP	2009	DBLP DOI BibTeX RDF
1	Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David 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
1	Patrick Schaller, Benedikt Schmidt, 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
1	Daniel Wasserrab, Denis Lohner, Gregor Snelting	On PDG-based noninterference and its modular proof.	PLAS	2009	DBLP DOI BibTeX RDF	modularity, program slicing, noninterference, correctness proof, program dependence graph
1	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
1	Moritz Kleine, Björn Bartels, Thomas Göthel, Sabine Glesner	Verifying the Implementation of an Operating System Scheduler.	TASE	2009	DBLP DOI BibTeX RDF
1	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
1	Javier de Dios, Ricardo Peña-Marí	A Certified Implementation on Top of the Java Virtual Machine.	FMICS	2009	DBLP DOI BibTeX RDF
1	Christoph Lüth, Dennis Walter	Certifiable Specification and Verification of C Programs.	FM	2009	DBLP DOI BibTeX RDF
1	David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt	Let's Get Physical: Models and Methods for Real-World Security Protocols.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Stefan Berghofer, Markus Reiter	Formalizing the Logic-Automaton Connection.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Jeremy E. Dawson, Alwen Tiu	Formalising Observer Theory for Environment-Sensitive Bisimulation.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	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
1	Rafal Kolanski, Gerwin Klein	Types, Maps and Separation Logic.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	René Thiemann, Christian Sternagel	Certification of Termination Proofs Using CeTA.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish	Mind the Gap.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Achim D. Brucker, Burkhart Wolff	Semantics, calculi, and analysis for object-oriented specifications.	Acta Inf.	2009	DBLP DOI BibTeX RDF
1	Jasmin Christian Blanchette	Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Interactive theorem provers, Huffman coding, Higher-order logic
1	Harvey Tuch	Formal Verification of C Systems Code.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	C, Separation logic, Interactive theorem proving
1	Amine Chaieb	Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
1	Christoph Sprenger, David A. Basin	Cryptographically-Sound Protocol-Model Abstractions.	CSF	2008	DBLP DOI BibTeX RDF	cryptographic soundness, formal methods, theorem proving, Cryptographic protocols, simulatability
1	Christian Urban, James Cheney, Stefan Berghofer	Mechanizing the Metatheory of LF.	LICS	2008	DBLP DOI BibTeX RDF	mechanized metatheory, logical frameworks, nominal logic
1	Bo Zhang	Formal Analysis of a Distributed Fault Tolerant Clock Synchronization Algorithm for Automotive Communication Systems.	EUROMICRO-SEAA	2008	DBLP DOI BibTeX RDF
1	Bo Zhang	Specifying and Verifying Timing Properties of a Time-triggered Protocol for In-vehicle Communication.	SNPD	2008	DBLP DOI BibTeX RDF
1	Sergey Tverdyshev, Eyad Alkassar	Efficient Bit-Level Model Reductions for Automated Hardware Verification.	TIME	2008	DBLP DOI BibTeX RDF
1	Tobias Nipkow	Linear Quantifier Elimination.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Temesghen Kahsai, Marino Miculan	Implementing Spi Calculus Using Nominal Techniques.	CiE	2008	DBLP DOI BibTeX RDF
1	Eyad Alkassar, Peter Böhm, Steffen Knapp	Formal Correctness of an Automotive Bus Controller Implementation at Gate-Level.	DIPES	2008	DBLP DOI BibTeX RDF
1	Michael Backes, Matthias Berg, Dominique Unruh	A Formal Language for Cryptographic Pseudocode.	LPAR	2008	DBLP DOI BibTeX RDF
1	Christian Urban, Bozhi Zhu	Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof.	RTA	2008	DBLP DOI BibTeX RDF
1	Florian Kammüller, Henry Sudhof	Composing Safely - A Type System for Aspects.	Software Composition	2008	DBLP DOI BibTeX RDF
1	Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff	HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier.	TPHOLs	2008	DBLP DOI BibTeX RDF
1	David Cock, Gerwin Klein, Thomas Sewell	Secure Microkernels, State Monads and Scalable Refinement.	TPHOLs	2008	DBLP DOI BibTeX RDF
1	Mike Gordon	Twenty Years of Theorem Proving for HOLs Past, Present and Future.	TPHOLs	2008	DBLP DOI BibTeX RDF
1	Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow	The Isabelle Framework.	TPHOLs	2008	DBLP DOI BibTeX RDF
1	Eyad Alkassar, Mark A. Hillebrand	Formal Functional Verification of Device Drivers.	VSTTE	2008	DBLP DOI BibTeX RDF
1	Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone	Verified Protection Model of the seL4 Microkernel.	VSTTE	2008	DBLP DOI BibTeX RDF
1	Rafal Kolanski, Gerwin Klein	Mapped Separation Logic.	VSTTE	2008	DBLP DOI BibTeX RDF
1	Amine Chaieb, Tobias Nipkow	Proof Synthesis and Reflection for Linear Arithmetic.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Proof synthesis, Linear arithmetic, Reflection