FMOODS
2007
13 years 6 months ago
2007
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...
CSFW
2010
IEEE
13 years 7 months ago
2010
IEEE
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...
TYPES
2000
Springer
13 years 8 months ago
2000
Springer
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...
TYPES
2004
Springer
13 years 9 months ago
2004
Springer
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...
CSFW
2006
IEEE
13 years 10 months ago
2006
IEEE
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 ...
SOFSEM
2010
Springer
14 years 1 months ago
2010
Springer
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...
ESORICS
2002
Springer
14 years 4 months ago
2002
Springer
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 ...
CADE
2008
Springer
14 years 4 months ago
2008
Springer
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 ...
POPL
2007
ACM
14 years 4 months ago
2007
ACM
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...
ICFP
2009
ACM
14 years 5 months ago
2009
ACM
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...