Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-35182-2_26
Title: Decision procedures over sophisticated fractional permissions
Authors: Bach, L.X.
Gherghina, C.
Hobor, A. 
Issue Date: 2012
Source: Bach, L.X.,Gherghina, C.,Hobor, A. (2012). Decision procedures over sophisticated fractional permissions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7705 LNCS : 368-385. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-35182-2_26
Abstract: Fractional permissions enable sophisticated management of resource accesses in both sequential and concurrent programs. Entailment checkers for formulae that contain fractional permissions must be able to reason about said permissions to verify the entailments. We show how entailment checkers for separation logic with fractional permissions can extract equation systems over fractional shares. We develop a set decision procedures over equations drawn from the sophisticated boolean binary tree fractional permission model developed by Dockins et al. [4]. We prove that our procedures are sound and complete and discuss their computational complexity. We explain our implementation and provide benchmarks to help understand its performance in practice. We detail how our implementation has been integrated into the HIP/SLEEK verification toolset. We have machine-checked proofs in Coq. ©Springer-Verlag 2012.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/40830
ISBN: 9783642351815
ISSN: 03029743
DOI: 10.1007/978-3-642-35182-2_26
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

7
checked on Dec 13, 2017

Page view(s)

86
checked on Dec 16, 2017

Google ScholarTM

Check

Altmetric


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