A decision procedure for separation logic in SMT

DOI10.1007/978-3-319-46520-3_16zbMath1398.68486arXiv1603.06844OpenAlexW2309670657MaRDI QIDQ1990511

Andrew Reynolds, Tim King, Radu Iosif, Cristina Serban

Publication date: 25 October 2018

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

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (6)

Program Verification with Separation Logic ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Strong-separation logic ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• SMT-LIB
• CVC4
• Infer
• Slide

This page was built for publication: A decision procedure for separation logic in SMT