Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

DOI10.1007/978-3-662-54434-1_23zbMATH Open1485.68068arXiv1610.07041OpenAlexW2543538425MaRDI QIDQ2988661FDOQ2988661

Christina Jansen, Christoph Matheja, Florian Zuleger, Jens Katelaan, Thomas Noll

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

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 protoype 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.

Full work available at URL: https://arxiv.org/abs/1610.07041

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• A semantics for concurrent separation logic
• An axiomatic basis for computer programming
• Permission accounting in separation logic
• Programming Languages and Systems
• Resources, concurrency, and local reasoning
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Compositional shape analysis by means of bi-abduction
• Separation Logic Modulo Theories
• Forest automata for verification of heap manipulation
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Shape Analysis for Composite Data Structures
• The Tree Width of Separation Logic with Recursive Definitions
• Compositional Entailment Checking for a Fragment of Separation Logic
• A decision procedure for satisfiability in separation logic with inductive predicates
• Automated Cyclic Entailment Proofs in Separation Logic
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• Model checking for symbolic-heap separation logic with inductive predicates
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
• Inference of Field-Sensitive Reachability and Cyclicity
• From Separation Logic to Hyperedge Replacement and Back
• Runtime Checking for Separation Logic

Cited In (7)

• Compositional satisfiability solving in separation logic
• Model checking for symbolic-heap separation logic with inductive predicates
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• Title not available (Why is that?)
• Decision problems in a logic for reasoning about reconfigurable distributed systems
• An efficient cyclic entailment procedure in a fragment of separation logic

Uses Software

• Predator
• VeriFast
• SLAyer
• HIP
• Smallfoot
• THOR
• Cyclist
• coreStar
• Infer
• Slide

This page was built for publication: Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988661)