A complete decision procedure for linearly compositional separation logic with data constraints

DOI10.1007/978-3-319-40229-1_36MaRDI QIDQ2817951zbMATH OpenOpenAlexFDO

Authors Xincai Gu, Taolue Chen, Zhilin Wu

Publication date 5 September 2016

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-40229-1_36

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Compositional entailment checking for a fragment of separation logic
• Compositional entailment checking for a fragment of separation logic
• Program Verification with Separation Logic
• Deciding entailments in inductive separation logic with tree automata
• A decision procedure for separation logic in SMT

Cites work

• A decision procedure for satisfiability in separation logic with inductive predicates
• Accurate invariant checking for programs manipulating lists and arrays with infinite data
• Automated cyclic entailment proofs in separation logic
• Automated theorem proving for assertions in separation logic with all connectives
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Compositional entailment checking for a fragment of separation logic
• Deciding entailments in inductive separation logic with tree automata
• Expressive completeness of separation logic with two variables and no separating conjunction
• Fast LCF-Style Proof Reconstruction for Z3
• Foundations for decision problems in separation logic with general inductive predicates
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• On automated lemma generation for separation logic with inductive definitions
• On the almighty wand
• Programming Languages and Systems
• Quantitative separation logic and programs with lists
• The tree width of separation logic with recursive definitions
• Tractable Reasoning in a Fragment of Separation Logic

Cited in

(15)

• Compositional entailment checking for a fragment of separation logic
• A separation logic with data: small models and automation
• A decision procedure for separation logic in SMT
• Reasoning about block-based cloud storage systems via separation logic
• Separation logic with linearly compositional inductive predicates and set data constraints
• Strong-separation logic
• Compositional satisfiability solving in separation logic
• Satisfiability of compositional separation logic with tree predicates and data constraints
• Compositional entailment checking for a fragment of separation logic
• Deciding entailments in inductive separation logic with tree automata
• Tractability of separation logic with inductive definitions: beyond lists
• An efficient cyclic entailment procedure in a fragment of separation logic
• Effective entailment checking for separation logic with inductive definitions
• Deciding satisfiability for overlaid symbolic heaps
• What is decidable in separation logic beyond progress, connectivity and establishment?

Describes a project that uses

Uses Software

• GRASShopper
• Infer
• HIP
• Slide

This page was built for publication: A complete decision procedure for linearly compositional separation logic with data constraints

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