Expressive completeness of separation logic in block-based cloud storage systems

DOI10.1016/J.TCS.2025.115372MaRDI QIDQ6956044zbMATH OpenFDO

Authors Tianyue Cao, Zhao Jin, Bowen Zhang, Yongzhi Cao, Hanpin Wang

Publication date 21 July 2025

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

Full work available at URL https://doi.org/10.1016/J.TCS.2025.115372

zbMATH Keywords

cloud storage systemsexpressivenessformal verificationseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Information storage and retrieval of data (68P20) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• An adaptation-complete proof system for local reasoning about cloud storage systems
• An axiomatic basis for computer programming
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• BI as an assertion language for mutable data structures
• Expressive completeness of separation logic with two variables and no separating conjunction
• Expressiveness results for an inductive logic of separated relations
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Hoare logic and auxiliary variables
• Mathematical Knowledge Management
• On the almighty wand
• On the Expressive Power of Graph Logic
• Programming Languages and Systems
• Reasoning about block-based cloud storage systems via separation logic
• Recompression: a simple and powerful technique for word equations
• Separating Graph Logic from MSO
• Solving equations with sequence variables and sequence functions
• The expressibility of languages and relations by word equations

This page was built for publication: Expressive completeness of separation logic in block-based cloud storage systems

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