An adaptation-complete proof system for local reasoning about cloud storage systems

DOI10.1016/J.TCS.2021.12.018MaRDI QIDQ2072067zbMATH OpenOpenAlexWikidataFDO

Authors Zhao Jin, B. Zhang, Lei Zhang, Yongzhi Cao, Hanpin Wang

Publication date 1 February 2022

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

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

zbMATH Keywords

cloud storage systemscompletenesslocal reasoningpredicate-transformation semanticsseparation logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Design and validation of cloud storage systems using formal methods
• On the completeness of modular proof systems
• Separation logic-based verification atop a binary-compatible filesystem model
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• A proof system for separation logic with magic wand

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• A proof system for separation logic with magic wand
• A sharp proof rule for procedures in WP semantics
• An axiomatic basis for computer programming
• BI as an assertion language for mutable data structures
• Biabduction (and related problems) in array separation logic
• Calculating sharp adaptation rules.
• Completeness and expressiveness of pointer program verification by separation logic
• Completeness for recursive procedures in separation logic
• Compositional shape analysis by means of bi-abduction
• Hoare logic and auxiliary variables
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 3751028 (Why is no real title available?)
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Local reasoning about a copying garbage collector
• Local reasoning about the presence of bugs: incorrectness separation logic
• Parametric completeness for separation theories
• Programming Languages and Systems
• Resources, concurrency, and local reasoning
• Soundness and Completeness of an Axiom System for Program Verification
• The Logic of Bunched Implications
• The specification statement
• Tools and Algorithms for the Construction and Analysis of Systems
• Verify heaps via unified model checking

Cited in

(3)

• Design and validation of cloud storage systems using formal methods
• Reasoning about block-based cloud storage systems via separation logic
• Expressive completeness of separation logic in block-based cloud storage systems

Describes a project that uses

Uses Software

• SLAyer
• Hadoop

This page was built for publication: An adaptation-complete proof system for local reasoning about cloud storage systems

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