Sciweavers

Share
FMOODS
2007
10 years 2 days ago
A Mechanized Model of the Theory of Objects
In this paper we present a formalization of Abadi’s and Cardelli’s theory of objects in the interactive theorem prover Isabelle/HOL. Our motivation is to build a mechanized HOL...
Ludovic Henrio, Florian Kammüller
CSFW
2010
IEEE
10 years 1 months ago
Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs
We embed an operational semantics for security protocols in the interactive theorem prover Isabelle/HOL and derive two strong protocol-independent invariants. These invariants allo...
Simon Meier, Cas J. F. Cremers, David A. Basin
TYPES
2000
Springer
10 years 2 months ago
Executing Higher Order Logic
We report on the design of a prototyping component for the theorem prover Isabelle/HOL. Specifications consisting of datatypes, recursive functions and inductive definitions are co...
Stefan Berghofer, Tobias Nipkow
TYPES
2004
Springer
10 years 4 months ago
Extracting a Normalization Algorithm in Isabelle/HOL
We present a formalization of a constructive proof of weak normalization for the simply-typed λ-calculus in the theorem prover Isabelle/HOL, and show how a program can be extracte...
Stefan Berghofer
CSFW
2006
IEEE
10 years 4 months ago
Cryptographically Sound Theorem Proving
We describe a faithful embedding of the Dolev-Yao model of Backes, Pfitzmann, and Waidner (CCS 2003) in the theorem prover Isabelle/HOL. This model is cryptographically sound in ...
Christoph Sprenger, Michael Backes, David A. Basin...
SOFSEM
2010
Springer
10 years 7 months ago
Finding and Certifying Loops
Abstract. The first part of this paper presents a new approach for automatically proving nontermination of string rewrite systems. We encode rewrite sequences as propositional for...
Harald Zankl, Christian Sternagel, Dieter Hofbauer...
ESORICS
2002
Springer
10 years 10 months ago
Formal Security Analysis with Interacting State Machines
We introduce the ISM approach, a framework for modeling and verifying reactive systems in a formal, even machine-checked, way. The framework has been developed for applications in ...
David von Oheimb, Volkmar Lotz
CADE
2008
Springer
10 years 11 months ago
Linear Quantifier Elimination
Abstract. This paper presents verified quantifier elimination procedures for dense linear orders (DLO), for real and for integer linear arithmetic. The DLO procedures are new. All ...
Tobias Nipkow
POPL
2007
ACM
10 years 11 months ago
Types, bytes, and separation logic
We present a formal model of memory that both captures the lowlevel features of C's pointers and memory, and that forms the basis for an expressive implementation of separati...
Harvey Tuch, Gerwin Klein, Michael Norrish
ICFP
2009
ACM
10 years 11 months ago
Experience report: seL4: formally verifying a high-performance microkernel
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. fication connects an abstract operational spe...
Gerwin Klein, Philip Derrin, Kevin Elphinstone
books