Reasoning about block-based cloud storage systems via separation logic
From MaRDI portal
Publication:2087457
DOI10.1016/j.tcs.2022.09.015OpenAlexW4298009049MaRDI QIDQ2087457
Yongzhi Cao, Zhao Jin, Hanpin Wang, Tianyue Cao, Bowen Zhang
Publication date: 21 October 2022
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2022.09.015
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Completeness for recursive procedures in separation logic
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Verify heaps via unified model checking
- An adaptation-complete proof system for local reasoning about cloud storage systems
- A decidable fragment in separation logic with inductive predicates and arithmetic
- Local reasoning about the presence of bugs: incorrectness separation logic
- Efficient verification of imperative programs using auto2
- Hash function design for cloud storage data auditing
- Biabduction (and related problems) in array separation logic
- Satisfiability of compositional separation logic with tree predicates and data constraints
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
- Model checking for symbolic-heap separation logic with inductive predicates
- Local reasoning about a copying garbage collector
- Deny-Guarantee Reasoning
- Finding Polynomial Loop Invariants for Probabilistic Programs
- Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
- A relational model of types-and-effects in higher-order concurrent separation logic
- Compositional Shape Analysis by Means of Bi-Abduction
- A proof system for separation logic with magic wand
- Programming Languages and Systems
