Completeness and expressiveness of pointer program verification by separation logic

DOI10.1016/J.IC.2019.03.002MaRDI QIDQ2417849zbMATH OpenOpenAlexWikidataFDO

Authors Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen

Publication date 29 May 2019

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2019.03.002

zbMATH Keywords

completeness theoremexpressiveness theoremHoare's logicinductive definitionsseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Completeness for recursive procedures in separation logic
• Completeness for a first-order abstract separation logic
• Expressive completeness of separation logic with two variables and no separating conjunction
• Computer Science Logic
• Program Verification with Separation Logic

Cites work

• Automated cyclic entailment proofs in separation logic
• Automated Verification of Shape and Size Properties Via Separation Logic
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• BI as an assertion language for mutable data structures
• Call-by-value and call-by-name dual calculi with inductive and coinductive types
• Completeness for recursive procedures in separation logic
• Computer Science Logic
• Context logic as modal logic, completeness and parametric inexpressivity
• Cyclic proofs of program termination in separation logic
• Elimination of spatial connectives in static spatial logics
• Enhancing Program Verification with Lemmas
• Expressiveness and the completeness of Hoare's logic
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• Foundations of Software Science and Computational Structures
• scientific article; zbMATH DE number 3868598 (Why is no real title available?)
• scientific article; zbMATH DE number 4033739 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Lifting abstract interpreters to quantified logical domains
• Program synthesis using realizability
• Programming Languages and Systems
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I

Cited in

(15)

• Verifying pointer and string analyses with region type systems
• An adaptation-complete proof system for local reasoning about cloud storage systems
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Completeness for recursive procedures in separation logic
• Completeness for a first-order abstract separation logic
• Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
• Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Extending propositional separation logic for robustness properties
• Expressive completeness of separation logic with two variables and no separating conjunction
• Programming Languages and Systems
• Computer Science Logic
• Parametric completeness for separation theories
• A proof system for separation logic with magic wand
• Dynamic separation logic

Describes a project that uses

Uses Software

• HIP

This page was built for publication: Completeness and expressiveness of pointer program verification by separation logic

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