Disjoint Fractional Permissions in Verification: Applications, Systems and Theory

Abstract

Fractional permissions are widely used to reason about shared resource ownership in concurrent program verification. Traditional rational models, however, weaken the disjointness principle central to Separation Logic. This thesis investigates the tree share model, a canonical Boolean binary tree structure equipped with a join operator (⊕) and a multiplication-like operator (./), as a principled alternative that preserves disjointness while supporting infinite split-ability and scalable permission manipulation. The work develops three pillars. First, we embed tree shares into Separation Logic to support advanced verification tasks such as bi-abduction, inductive predicates, and precision reasoning. Second, we design sound and complete decision procedures for tree-share constraints and integrate them into the HIP/SLEEK verification toolset. Third, we establish precise decidability and complexity results for fragments of the tree-share structure, revealing connections to Boolean algebras and string concatenation. Together, these contributions provide a rigorous theoretical and practical foundation for disjoint fractional permissions in concurrent program verification.

Cite this paper

@phdthesis{le2017phd,
  author = {Le, Xuan-Bach},
  title  = {Disjoint Fractional Permissions in Verification: Applications, Systems and Theory},
  school = {National University of Singapore},
  year   = {2017},
  month  = {September}
}