%0 Conference Proceedings
%T Heap-Dependent Expressions in Separation Logic
%+ Catholic University of Leuven = Katholieke Universiteit Leuven (KU Leuven)
%A Smans, Jan
%A Jacobs, Bart
%A Piessens, Frank
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE)
%C Amsterdam, Netherlands
%Y John Hatcliff; Elena Zucca
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-6117
%P 170-185
%8 2010-06-07
%D 2010
%R 10.1007/978-3-642-13464-7_14
%Z Computer Science [cs]/Digital Libraries [cs.DL]Conference papers
%X 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.
%G English
%2 https://inria.hal.science/hal-01055155/document
%2 https://inria.hal.science/hal-01055155/file/61170168.pdf
%L hal-01055155
%U https://inria.hal.science/hal-01055155
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-LNCS-6117
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-FMOODS
%~ IFIP-2010