Please use this identifier to cite or link to this item:
|Title:||Decision procedures over sophisticated fractional permissions||Authors:||Bach, L.X.
|Issue Date:||2012||Citation:||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. . 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.
checked on Sep 20, 2022
checked on Sep 22, 2022
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.