| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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 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.
Cited literature [15 references]
https://hal.inria.fr/hal-01055155
Contributor : Hal Ifip <>
Submitted on : Monday, August 11, 2014 - 4:31:35 PM
Last modification on : Thursday, February 21, 2019 - 10:31:46 AM
Long-term archiving on: : Wednesday, November 26, 2014 - 10:15:40 PM
Contributor : Hal Ifip <>
Submitted on : Monday, August 11, 2014 - 4:31:35 PM
Last modification on : Thursday, February 21, 2019 - 10:31:46 AM
Long-term archiving on: : Wednesday, November 26, 2014 - 10:15:40 PM
File
61170168.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License