Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/138215
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
Source: 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:
File Description SizeFormatAccess SettingsVersion 
thesis.pdf1.49 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

15
checked on Jan 21, 2018

Download(s)

3
checked on Jan 21, 2018

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.