Go to page
 

Bibliographic Metadata

Title
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
AuthorJansen, Christina ; Katelaan, Jens ; Matheja, Christoph ; Noll, Thomas ; Zuleger, Florian
Published in
Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings : Yang, Hongseok, Berlin, Heidelberg, 2017, page 611-638
Published2017
LanguageEnglish
SeriesLecture Notes in Computer Science ; 10201
Document typeArticle in a collected edition
Project-/ReportnumberAustrian Science Fund (FWF): W1255-N23
Project-/ReportnumberAustrian Science Fund (FWF): National Research Network S11403-N23 (RiSE)
Project-/ReportnumberDeutsche Forschungsgemeinschaft (DFG): Grant NO. 401/2-1
ISBN9783662544334
URNurn:nbn:at:at-ubtuw:3-3660 Persistent Identifier (URN)
DOI10.1007/978-3-662-54434-1_23 
Restriction-Information
 The work is publicly available
Files
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic [0.55 mb]
Links
Reference
Classification
Abstract (English)

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.

Note
Note
Stats
The PDF-Document has been downloaded 11 times.