CSL
2008
Springer
13 years 6 months ago
2008
Springer
We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SL) and its fragments. SL can specify pr...
ECOOP
2010
Springer
13 years 8 months ago
2010
Springer
Specifications of Object-Oriented programs conventionally employ Boolean expressions of the programming language for assertions. Programming errors can be discovered by checking at...
CSL
2006
Springer
13 years 8 months ago
2006
Springer
Separation Logic is a sub-structural logic that supports local reasoning for imperative programs. It is designed to elegantly describe sharing and aliasing properties of heap struc...
CSL
2004
Springer
13 years 8 months ago
2004
Springer
Using separation logic, this paper presents three Hoare logics (corresponding to different notions of correctness) for the simple While language extended with commands for heap acc...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
This paper proposes a modal extension of Separation Logic [8, 11] for reasoning about data-parallel programs that manipulate heap allocated linked data structures. Separation Logi...
ITP
2010
13 years 8 months ago
2010
We present a formalisation of separation logic which, by avoiding the use of existential quantifiers, allows proofs that only use standard equational rewriting methods as found in...
APLAS
2007
ACM
13 years 8 months ago
2007
ACM
Abstract. We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not po...
CONCUR
2004
Springer
13 years 10 months ago
2004
Springer
In this paper we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs.
CONCUR
2004
Springer
13 years 10 months ago
2004
Springer
We present a trace semantics for a language of parallel programs which share access to mutable data. We introduce a resource-sensitive logic for partial correctness, based on a re...
CAV
2004
Springer
13 years 10 months ago
2004
Springer
Abstract. Separation Logic consists of a Boolean combination of predicates of the form vi ≥ vj +c where c is a constant and vi, vj are variables of some ordered infinite type li...