Completeness for recursive procedures in separation logic

DOI10.1016/J.TCS.2016.04.004MaRDI QIDQ278747zbMATH OpenOpenAlexFDO

Authors Makoto Tatsuta, Mahmudul Faisal Al Ameen

Publication date 2 May 2016

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2016.04.004

zbMATH Keywords

completenessHoare logicrecursive proceduresseparation logic

Mathematics Subject Classification ID

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

Recommendations

• Completeness and expressiveness of pointer program verification by separation logic
• scientific article; zbMATH DE number 1948157
• scientific article; zbMATH DE number 3888900
• Frame rule for mutually recursive procedures manipulating pointers
• scientific article; zbMATH DE number 1500648

Cites work

• scientific article; zbMATH DE number 3868598 (Why is no real title available?)
• An axiomatic basis for computer programming
• Automated Verification of Shape and Size Properties Via Separation Logic
• BI as an assertion language for mutable data structures
• Enhancing Program Verification with Lemmas
• Expressiveness and the completeness of Hoare's logic
• Logic in Computer Science
• Programming Languages and Systems
• Separation and information hiding
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(8)

• Completeness proof by semantic diagrams for transitive closure of accessibility relation
• Frame rule for mutually recursive procedures manipulating pointers
• Completeness and expressiveness of pointer program verification by separation logic
• Termination assertions for recursive programs: Completeness and axiomatic definability
• Completeness issues in RUE-NRF deduction: The undecidability of viability
• An adaptation-complete proof system for local reasoning about cloud storage systems
• Completeness and Decidability in Sequence Logic
• Reasoning about block-based cloud storage systems via separation logic

Describes a project that uses

Uses Software

• Smallfoot
• HIP

This page was built for publication: Completeness for recursive procedures in separation logic

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