A separation logic with data: small models and automation

DOI10.1007/978-3-319-94205-6_30MaRDI QIDQ1799106zbMATH OpenOpenAlexFDO

Authors Jens Katelaan, Dejan Jovanović, Georg Weissenbacher

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94205-6_30

Mathematics Subject Classification ID

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

Recommendations

• A complete decision procedure for linearly compositional separation logic with data constraints
• Deciding entailments in inductive separation logic with tree automata
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Tractable Reasoning in a Fragment of Separation Logic
• The tree width of separation logic with recursive definitions

Cited in

(15)

• Make flows small again: revisiting the flow framework
• A Formalisation of Smallfoot in HOL
• scientific article; zbMATH DE number 7561347 (Why is no real title available?)
• Runtime Checking for Separation Logic
• A simple separation logic
• Deciding entailments in inductive separation logic with tree automata
• The tree width of separation logic with recursive definitions
• Tree-like grammars and separation logic
• Compositional satisfiability solving in separation logic
• Computer Aided Verification
• An efficient cyclic entailment procedure in a fragment of separation logic
• Tools and Algorithms for the Construction and Analysis of Systems
• Foundations of Software Science and Computational Structures
• Models and Separation Logics for Resource Trees
• Strong-separation logic

Describes a project that uses

Uses Software

• z3

This page was built for publication: A separation logic with data: small models and automation

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