Separation logic with one quantified variable

DOI10.1007/978-3-319-06686-8_10MaRDI QIDQ4981154zbMATH OpenOpenAlexFDO

Authors Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry

Publication date 24 June 2014

Published in Computer Science - Theory and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-06686-8_10

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Separation logic with one quantified variable
• On the almighty wand
• On the Almighty Wand
• Quantitative Separation Logic and Programs with Lists
• Expressive completeness of separation logic with two variables and no separating conjunction

Cited in

(20)

• Semipositivity in separation logic with two variables
• Prenex separation logic with one selector field
• Strong-separation logic
• Separation logic with one quantified variable
• Variables as resource in separation logic
• Two-Variable Separation Logic and Its Inner Circle
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• scientific article; zbMATH DE number 5994600 (Why is no real title available?)
• Completeness for a first-order abstract separation logic
• Automated theorem proving for assertions in separation logic with all connectives
• Quantitative Separation Logic and Programs with Lists
• On the almighty wand
• Separation logics and modalities: a survey
• Expressive completeness of separation logic with two variables and no separating conjunction
• Expressive completeness of separation logic with two variables and no separating conjunction
• Foundations of Software Science and Computational Structures
• A proof procedure for separation logic with inductive definitions and data
• An algebraic glimpse at bunched implications and separation logic
• An EXPTIME-complete entailment problem in separation logic
• Quantitative separation logic and programs with lists

This page was built for publication: Separation logic with one quantified variable

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