Title: | Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic | Language: | English | Authors: | Jansen, Christina Katelaan, Jens Matheja, Christoph Noll, Thomas Zuleger, Florian |
Issue Date: | 2017 | Abstract: | We introduce heap automata, a formalism for automatic reasoning about robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates. Robustness properties, such as satisfiability, reachability, and acyclicity, are important for a wide range of reasoning tasks in automated program analysis and verification based on separation logic. Previously, such properties have appeared in many places in the separation logic literature, but have not been studied in a systematic manner. In this paper, we develop an algorithmic framework based on heap automata that allows us to derive asymptotically optimal decision procedures for a wide range of robustness properties in a uniform way. We implemented a prototype of our framework and obtained promising results for all of the aforementioned robustness properties. Further, we demonstrate the applicability of heap automata beyond robustness properties. We apply our algorithmic framework to the model checking and the entailment problem for symbolic-heap separation logic. |
URI: | https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3660 http://hdl.handle.net/20.500.12708/913 |
Library ID: | AC15094525 | ISBN: | 9783662544334 | Organisation: | E192 - Institut für Logic and Computation | Publication Type: | Inproceedings Konferenzbeitrag |
Appears in Collections: | Conference Paper |
Files in this item:
File | Description | Size | Format | |
---|---|---|---|---|
Jansen Christina - 2017 - Unified Reasoning About Robustness Properties of...pdf | 571.3 kB | Adobe PDF | ![]() View/Open |
Page view(s)
21
checked on Apr 15, 2021
Download(s)
156
checked on Apr 15, 2021

Google ScholarTM
Check
Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.