Title: Heap-dependent expressions in separation logic
Authors: Smans, Jan ×
Jacobs, Bart
Piessens, Frank #
Issue Date: 7-Jun-2010
Publisher: Springer-Verlag
Host Document: Formal Techniques for Distributed Systems vol:6117 pages:170-185
Conference: FMOODS/FORTE edition:30 location:Amsterdam, Netherlands date:7-9 June 2010
Abstract: Separation logic is a popular specification language for imperative programs where the heap can only be mentioned through points-to assertions. However, separation logic's take on assertions does not match well with the classical view of assertions as boolean, side effect-free, 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 effect-free 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.
ISBN: 978-3-642-13463-0
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
forte2010.pdf Published 219KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science