Proof automation for functional correctness in separation logic

DOI10.1093/logcom/exu032zbMath1344.68209OpenAlexW2325932479MaRDI QIDQ5739977

Gudmund Grov, Andrew Ireland, Ewen Maclean

Publication date: 7 July 2016

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/20001869/jlc.pdf

zbMATH Keywords

substructural logicautomated theorem provingseparation logicproof planninginvariant discoveryfunctional correctness

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Related Items (2)

Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ A versatile concept for the analysis of loops

Uses Software

• Isabelle
• IsaPlanner
• Smallfoot

This page was built for publication: Proof automation for functional correctness in separation logic