Author name cluster

Tianyue Cao

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

TCS Journal 2025 Journal Article

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

Tianyue Cao
Zhao Jin
Bowen Zhang
Yongzhi Cao
Hanpin Wang

Block-based cloud storage systems are widely used to store big data. Although they are highly fault-tolerant, the occurrence of bugs is still inevitable. Separation logic was proposed for mutable data structures, and can be used to verify block-based cloud storage systems. Hoare-style proof system has been constructed to verify these systems, and has been implemented in Coq. However, expressiveness of the assertion language in this formal system has not been fully studied. To fill this gap, we show the expressive completeness of separation logic in block-based cloud storage system, and prove the following three main consequences: (1) this logic is strictly more expressive than first-order logic, (2) this logic is as expressive as separation logic, and (3) this logic is as expressive as weak second-order logic with sequences.

Details DOI

TCS Journal 2022 Journal Article

Reasoning about block-based cloud storage systems via separation logic

Zhao Jin
Bowen Zhang
Tianyue Cao
Yongzhi Cao
Hanpin Wang

Owing to the massive growth in the storage demands of big data, cloud storage systems emerge at a historic moment, among which block-based cloud storage systems (BCSSs) are typical. Compared with traditional storage systems, BCSSs have many advantages, such as higher capacity, lower cost, and better scalability. BCSSs are also much more complex and error prone than traditional systems, and therefore, their reliability is a significant concern. Correctness is the most basic requirement for reliability. Therefore, it is of great significance to study BCSS program correctness verification to establish the theoretical basis for cloud storage systems. In this paper, we propose a novel framework based on separation logic (SL) to verify the correctness of BCSS management programs. We first construct a two-tier heap structure as the formal model of the storage architecture for BCSSs and present a modelling language based on this structure to describe the program execution. We then define assertion pairs to describe the properties of the two-tier structure. The two components of an assertion pair affect each other, producing several interesting properties. Finally, we propose a Hoare-style proof system to reason about BCSS programs and establish its soundness. We also demonstrate our proof system's uniqueness, usability, and scalability by verifying several real-world BCSS sample programs. In summary, this work presents a systematic approach that can be used to effectively solve BCSS program verification problems, and provides an SL-based logical modelling strategy, specifically to build its consistency with the actual behaviour of BCSSs.

Details DOI

NeurIPS Conference 2021 Conference Paper

Learning to Learn Graph Topologies

Xingyue Pu
Tianyue Cao
Xiaoyun Zhang
Xiaowen Dong
Siheng Chen

Learning a graph topology to reveal the underlying relationship between data entities plays an important role in various machine learning and data analysis tasks. Under the assumption that structured data vary smoothly over a graph, the problem can be formulated as a regularised convex optimisation over a positive semidefinite cone and solved by iterative algorithms. Classic methods require an explicit convex function to reflect generic topological priors, e. g. the $\ell_1$ penalty for enforcing sparsity, which limits the flexibility and expressiveness in learning rich topological structures. We propose to learn a mapping from node data to the graph structure based on the idea of learning to optimise (L2O). Specifically, our model first unrolls an iterative primal-dual splitting algorithm into a neural network. The key structural proximal projection is replaced with a variational autoencoder that refines the estimated graph with enhanced topological properties. The model is trained in an end-to-end fashion with pairs of node data and graph samples. Experiments on both synthetic and real-world data demonstrate that our model is more efficient than classic iterative algorithms in learning a graph with specific topological properties.

PDF Details

AAAI Conference 2019 Short Paper

APRP: An Anonymous Propagation Method in Bitcoin Network

Yuhang Yao
Xiao Zeng
Tianyue Cao
Luoyi Fu
Xinbing Wang

Due to little attention given to anonymous protection against eavesdropping attacks in Bitcoin network, this paper initiatively proposes a solution to Bitcoin anonymization based on network structure. We first present a general adversarial network model for formulizing deanonymization attack, then present a novel propagation method APRP(Adaptive PageRank Propagation) that adopts PageRank as propagation delay factor and constantly adjusts PR-value of nodes to adapt to network dynamics. Experiments on both simulated and real Bitcoin networks confirm the superiority of APRP in terms of 20-50% performance enhancement under various deanonymization attacks.

PDF Details