Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

DOI10.1007/978-3-662-54434-1_23zbMath1485.68068arXiv1610.07041OpenAlexW2543538425MaRDI QIDQ2988661

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)

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

Mathematics Subject Classification ID

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

Related Items

An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Compositional satisfiability solving in separation logic ⋮ Unnamed Item ⋮ Decision problems in a logic for reasoning about reconfigurable distributed systems ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Uses Software

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

Cites Work

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