Separation Logic Modulo Theories

DOI10.1007/978-3-319-03542-0_7zbMath1426.68058arXiv1303.2489OpenAlexW1841862047MaRDI QIDQ2937786

Andrey Rybalchenko, Juan Antonio Navarro Pérez

Publication date: 12 January 2015

Published in: Programming Languages and Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Related Items (14)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ A First-Order Logic with Frames ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic ⋮ Separation logic with one quantified variable ⋮ Automated mutual induction proof in separation logic ⋮ Horn Clause Solvers for Program Verification ⋮ Separation logics and modalities: a survey ⋮ A proof procedure for separation logic with inductive definitions and data ⋮ Compositional entailment checking for a fragment of separation logic ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Strong-separation logic ⋮ Compositional satisfiability solving in separation logic

This page was built for publication: Separation Logic Modulo Theories