Sciweavers

Share
FORTE
2010

Heap-Dependent Expressions in Separation Logic

9 years 11 months ago
Heap-Dependent Expressions in Separation Logic
Abstract. Separation logic is a popular specification language for imperative programs where the heap can only be mentioned through pointsto assertions. However, separation logic's take on assertions does not match well with the classical view of assertions as boolean, side effectfree, potentially heap-dependent expressions from the host programming language familiar to many developers. In this paper, we propose a variant of separation logic where side effectfree expressions from the host programming language, such as pointer dereferences and invocations of pure methods, can be used in assertions. We modify the symbolic execution-based verification algorithm used in Smallfoot to support mechanized checking of our variant of separation logic. We have implemented this algorithm in a tool and used the tool to verify some interesting programming patterns.
Jan Smans, Bart Jacobs, Frank Piessens
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2010
Where FORTE
Authors Jan Smans, Bart Jacobs, Frank Piessens
Comments (0)
books