| Fractional permissions enable sophisticated accounting reasoning over resource ownership in Concurrent Separation Logic (CSL). The common permission model uses rational numbers in (0,1] as permissions and addition for splitting/joining permissions.However, this model poses technical challenges for compositional reasoning. As a result, there has been substantial work in proposing better models recently. In this thesis, we propose the disjoint permissions to fix the shortcomings of rational permissions. We conduct a comprehensive study of the disjoint permissions via three different aspects: applications, systems, and theory. In particular, we develop an expressive proof system with disjoint permissions that can handle sophisticated verification tasks like induction and bi-abduction. Also, we devise complete and certified decision procedures to solve different types of permissions constraints required by verification tools. For theory aspect, we obtain various decidability and complexity results over the theory of disjoint permissions using connections to automatic structures, word equations and Boolean Algebras. |
