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

DOI10.1016/j.tcs.2021.12.018OpenAlexW4200151489WikidataQ115440450 ScholiaQ115440450MaRDI QIDQ2072067

Bowen Zhang, Yongzhi Cao, Hanpin Wang, Zhao Jin, Lei Zhang

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

completenessseparation logiclocal reasoningcloud storage systemspredicate-transformation semantics

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items

Reasoning about block-based cloud storage systems via separation logic

Uses Software

• Hadoop
• SLAyer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Completeness for recursive procedures in separation logic
• Resources, concurrency, and local reasoning
• A sharp proof rule for procedures in WP semantics
• Calculating sharp adaptation rules.
• Hoare logic and auxiliary variables
• Verify heaps via unified model checking
• Local reasoning about the presence of bugs: incorrectness separation logic
• Biabduction (and related problems) in array separation logic
• Completeness and expressiveness of pointer program verification by separation logic
• A lattice-theoretical fixpoint theorem and its applications
• Iris
• Local reasoning about a copying garbage collector
• Soundness and Completeness of an Axiom System for Program Verification
• The Logic of Bunched Implications
• The specification statement
• BI as an assertion language for mutable data structures
• Compositional Shape Analysis by Means of Bi-Abduction
• Parametric completeness for separation theories
• A proof system for separation logic with magic wand
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Tools and Algorithms for the Construction and Analysis of Systems