Search results for "Isabelle/HOL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
20	Florian Kammüller, Henry Sudhof	Composing Safely - A Type System for Aspects.	SC@ETAPS	2008	DBLP DOI BibTeX RDF
20	Eyad Alkassar, Peter Böhm, Steffen Knapp	Formal Correctness of an Automotive Bus Controller Implementation at Gate-Level.	DIPES	2008	DBLP DOI BibTeX RDF
20	Sergey Tverdyshev, Eyad Alkassar	Efficient Bit-Level Model Reductions for Automated Hardware Verification.	TIME	2008	DBLP DOI BibTeX RDF
20	Christian Urban, Bozhi Zhu	Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof.	RTA	2008	DBLP DOI BibTeX RDF
20	Temesghen Kahsai, Marino Miculan	Implementing Spi Calculus Using Nominal Techniques.	CiE	2008	DBLP DOI BibTeX RDF
20	Bo Zhang	Formal Analysis of a Distributed Fault Tolerant Clock Synchronization Algorithm for Automotive Communication Systems.	EUROMICRO-SEAA	2008	DBLP DOI BibTeX RDF
20	Vaidas Gasiunas, Mira Mezini, Klaus Ostermann	Dependent classes.	OOPSLA	2007	DBLP DOI BibTeX RDF	dependent classes, variability, dynamic dispatch, multimethods, multiple dispatch, virtual classes
20	Yongjian Li	Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols.	SAC	2007	DBLP DOI BibTeX RDF	parameterized verification, theorem proving, symmetry
20	Christoph Benzmüller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier	Deep Inference for Automated Proof Tutoring?	KI	2007	DBLP DOI BibTeX RDF
20	Lennart Beringer, Martin Hofmann 0001	Secure information flow and program logics.	CSF	2007	DBLP DOI BibTeX RDF
20	Harvey Tuch, Gerwin Klein, Michael Norrish	Types, bytes, and separation logic.	POPL	2007	DBLP DOI BibTeX RDF	C, separation logic, interactive theorem proving
20	Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter	Translation Validation of System Abstractions.	RV	2007	DBLP DOI BibTeX RDF
20	Alexander Krauss 0001	Certified Size-Change Termination.	CADE	2007	DBLP DOI BibTeX RDF
20	Julien Schmaltz	A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware.	FMCAD	2007	DBLP DOI BibTeX RDF
20	Yongjian Li, Jun Pang 0001	Extending the Strand Space Method to Verify Kerberos V.	PDCAT	2007	DBLP DOI BibTeX RDF
20	Ulrich Berger 0001, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg	Program Extraction from Normalization Proofs.	Stud Logica	2006	DBLP DOI BibTeX RDF	Normalization by evaluation, program extraction from proofs, realizability, typed lambda calculus
20	Gerwin Klein, Tobias Nipkow	A machine-checked model for a Java-like language, virtual machine, and compiler.	ACM Trans. Program. Lang. Syst.	2006	DBLP DOI BibTeX RDF	Java, theorem proving, operational semantics
20	Philipp Rümmer	Sequential, Parallel, and Quantified Updates of First-Order Structures.	LPAR	2006	DBLP DOI BibTeX RDF
20	Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip	An operational semantics and type safety prooffor multiple inheritance in C++.	OOPSLA	2006	DBLP DOI BibTeX RDF	semantics, C++, type safety, multiple inheritance
20	Amine Chaieb	Proof-Producing Program Analysis.	ICTAC	2006	DBLP DOI BibTeX RDF
20	Tobias Nipkow	Verifying a Hotel Key Card System.	ICTAC	2006	DBLP DOI BibTeX RDF
20	Christoph Sprenger 0001, Michael Backes 0001, David A. Basin, Birgit Pfitzmann, Michael Waidner	Cryptographically Sound Theorem Proving.	CSFW	2006	DBLP DOI BibTeX RDF
20	M. C. Dharmadeep, K. Gopinath	Proactive Leader Election in Asynchronous Shared Memory Systems.	ATVA	2006	DBLP DOI BibTeX RDF
20	Lennart Beringer, Martin Hofmann 0001	A Bytecode Logic for JML and Types.	APLAS	2006	DBLP DOI BibTeX RDF
20	Huabing Yang, Xingyuan Zhang, Yuanyuan Wang	A Correctness Proof of the DSR Protocol.	MSN	2006	DBLP DOI BibTeX RDF
20	Huabing Yang, Xingyuan Zhang, Yuanyuan Wang	A correctness proof of the SRP protocol.	IPDPS	2006	DBLP DOI BibTeX RDF
20	Alexander Krauss 0001	Partial Recursive Functions in Higher-Order Logic.	IJCAR	2006	DBLP DOI BibTeX RDF
20	Simon Winwood, Gerwin Klein, Manuel M. T. Chakravarty	On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors.	LOPSTR	2006	DBLP DOI BibTeX RDF
20	Tobias Nipkow, Lawrence C. Paulson	Proof Pearl: Defining Functions over Finite Sets.	TPHOLs	2005	DBLP DOI BibTeX RDF
20	Veronika Ortner, Norbert Schirmer	Verification of BDD Normalization.	TPHOLs	2005	DBLP DOI BibTeX RDF
20	Martin Wildmoser, Tobias Nipkow	Asserting Bytecode Safety.	ESOP	2005	DBLP DOI BibTeX RDF
20	Yongjian Li	The Inductive Approach to Strand Space.	FORTE	2005	DBLP DOI BibTeX RDF
20	Zhouyi Zhou, Bin Liang, Li Jiang, Wenchang Shi, Yeping He	A Formal Description of SECIMOS Operating System.	MMM-ACNS	2005	DBLP DOI BibTeX RDF
20	Kerry Trentelman	Proving Correctness of JavaCard DL Taclets using Bali.	SEFM	2005	DBLP DOI BibTeX RDF
20	Gilles Barthe, Leonor Prensa Nieto	Formally verifying information flow type systems for concurrent and thread systems.	FMSE	2004	DBLP DOI BibTeX RDF	machine-checked proofs, concurrency, noninterference
20	David Aspinall 0001, Lennart Beringer, Martin Hofmann 0001, Hans-Wolfgang Loidl, Alberto Momigliano	A Program Logic for Resource Verification.	TPHOLs	2004	DBLP DOI BibTeX RDF
20	Tjark Weber	Towards Mechanized Program Verification with Separation Logic.	CSL	2004	DBLP DOI BibTeX RDF	Separation Logic, Interactive Theorem Proving, Formal Program Verification
20	David A. Basin, Stefan Friedrich 0001, Marek Gawkowski	Bytecode Verification by Model Checking.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	model checking, static analysis, type safety, bytecode verification
20	Gerwin Klein, Martin Wildmoser	Verified Bytecode Subroutines.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	Java, theorem proving, subroutines, dataflow analysis, Isabelle, bytecode verification
20	Gerwin Klein, Martin Wildmoser	Verified Bytecode Subroutines.	TPHOLs	2003	DBLP DOI BibTeX RDF
20	Thomas A. Kuhn, David von Oheimb	Interacting State Machines for Mobility.	FME	2003	DBLP DOI BibTeX RDF	dynamic communication, boxed ambients, Interacting State Machines, verification, mobility, mobile agents, formal modeling
20	Alberto Momigliano, Simon Ambler	Multi-level Meta-reasoning with Higher-Order Abstract Syntax.	FoSSaCS	2003	DBLP DOI BibTeX RDF
20	Koji Okuma, Yasuhiko Minamide	Executing Verified Compiler Specification.	APLAS	2003	DBLP DOI BibTeX RDF
20	Alberto Momigliano, Alwen Fernanto Tiu	Induction and Co-induction in Sequent Calculus.	TYPES	2003	DBLP DOI BibTeX RDF
20	Farhad Mehta, Tobias Nipkow	Proving Pointer Programs in Higher-Order Logic.	CADE	2003	DBLP DOI BibTeX RDF
20	David von Oheimb, Georg Walter, Volkmar Lotz	A Formal Security Model of the Infineon SLE 88 Smart Card Memory Managment.	ESORICS	2003	DBLP DOI BibTeX RDF
20	David A. Basin, Stefan Friedrich 0001, Marek Gawkowski	Verified Bytecode Model Checkers.	TPHOLs	2002	DBLP DOI BibTeX RDF
20	Gertrud Bauer, Tobias Nipkow	The 5 Colour Theorem in Isabelle/Isar.	TPHOLs	2002	DBLP DOI BibTeX RDF
20	Tobias Nipkow	Hoare Logics for Recursive Procedures and Unbounded Nondeterminism.	CSL	2002	DBLP DOI BibTeX RDF
20	Riccardo Mattolini, Paolo Nesi	An Interval Logic for Real-Time System Specification.	IEEE Trans. Software Eng.	2001	DBLP DOI BibTeX RDF	real-time systems, first order logic, verification and validation, Formal specification language, temporal interval logic
20	Steffen Helke, Thomas Santen	Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries.	FME	2001	DBLP DOI BibTeX RDF
20	Giampaolo Bella, Lawrence C. Paulson	A Proof of Non-repudiation.	Security Protocols Workshop	2001	DBLP DOI BibTeX RDF
20	Tobias Nipkow	Verified Bytecode Verifiers.	FoSSaCS	2001	DBLP DOI BibTeX RDF
20	René Vestergaard, James Brotherston	A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names.	RTA	2001	DBLP DOI BibTeX RDF
20	Pierfrancesco Bellini, Paolo Nesi	Communicating TILCO: A Model for Real-Time System Specification.	ICECCS	2001	DBLP DOI BibTeX RDF	real-time systems, first order logic, verification and validation, formal specification language, temporal interval logic
20	Stefan Berghofer, Tobias Nipkow	Executing Higher Order Logic.	TYPES	2000	DBLP DOI BibTeX RDF
20	Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano	Formal Verification of Cardholder Registration in SET.	ESORICS	2000	DBLP DOI BibTeX RDF
20	Tobias Nipkow	Verified Lexical Analysis.	TPHOLs	1998	DBLP DOI BibTeX RDF
20	Lawrence C. Paulson	Proving Properties of Security Protocols by Induction.	CSFW	1997	DBLP DOI BibTeX RDF
20	Tobias Nipkow	Winskel is (Almost) Right: Towards a Mechanized Semantics Textbook.	FSTTCS	1996	DBLP DOI BibTeX RDF