Please use this identifier to cite or link to this item:
|Title:||DISJOINT FRACTIONAL PERMISSIONS IN VERIFICATION: APPLICATIONS, SYSTEMS AND THEORY||Authors:||LE XUAN BACH||Keywords:||Separation Logic, Computational Complexity, Word Equation, Decision Procedure, Verification, Fractional Permissions||Issue Date:||14-Aug-2017||Citation:||LE XUAN BACH (2017-08-14). DISJOINT FRACTIONAL PERMISSIONS IN VERIFICATION: APPLICATIONS, SYSTEMS AND THEORY. ScholarBank@NUS Repository.||Abstract:||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.||URI:||http://scholarbank.nus.edu.sg/handle/10635/138215|
|Appears in Collections:||Ph.D Theses (Open)|
Show full item record
Files in This Item:
|thesis.pdf||1.49 MB||Adobe PDF|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.