Compositional entailment checking for a fragment of separation logic
type: Item
instance of: scholarly article
title: Compositional entailment checking for a fragment of separation logic
zbMATH Open document ID: 1377.68073
author: Constantin Enea
author: Ondřej Lengál
author: Mihaela Sighireanu
author: Tomáš Vojnar
published in: Formal Methods in System Design
publication date: 2018-01-08T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 6823096
zbMATH Keywords: program analysis
zbMATH Keywords: separation logic
zbMATH Keywords: decision procedure
zbMATH Keywords: tree automata
describes a project that uses: Smallfoot
describes a project that uses: VATA
describes a project that uses: Slide
describes a project that uses: MTBDD
describes a project that uses: Cyclist
MaRDI profile type: Publication
full work available at URL: s10703-017-0289-4
OpenAlex ID: W46575596
cites work: Shape Analysis for Composite Data Structures
cites work: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
cites work: A decision procedure for satisfiability in separation logic with inductive predicates
cites work: Q4474211
cites work: Automated verification of shape, size and bag properties via user-defined predicates in separation logic
cites work: Tractable Reasoning in a Fragment of Separation Logic
cites work: Compositional Entailment Checking for a Fragment of Separation Logic
cites work: Compositional Invariant Checking for Overlaid and Nested Linked Lists
cites work: On Automated Lemma Generation for Separation Logic with Inductive Definitions
cites work: Q3666827
cites work: A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
cites work: The Tree Width of Separation Logic with Recursive Definitions
cites work: Deciding Entailments in Inductive Separation Logic with Tree Automata
cites work: BI as an assertion language for mutable data structures
cites work: Satisfiability Modulo Heap-Based Programs
cites work: VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata
cites work: Separation Logic Modulo Theories
DOI: 10.1007/S10703-017-0289-4
description: scientific article; zbMATH DE number 6823096