Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-319-89884-1_14
DC FieldValue
dc.titleLogical reasoning for disjoint permissions
dc.contributor.authorLe X.-B.
dc.contributor.authorHobor A.
dc.date.accessioned2020-09-09T04:13:49Z
dc.date.available2020-09-09T04:13:49Z
dc.date.issued2018
dc.identifier.citationLe X.-B., Hobor A. (2018). Logical reasoning for disjoint permissions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 10801 LNCS : 385-414. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-319-89884-1_14
dc.identifier.issn0302-9743
dc.identifier.urihttps://scholarbank.nus.edu.sg/handle/10635/175138
dc.description.abstractResource sharing is a fundamental phenomenon in concurrent programming where several threads have permissions to access a common resource. Logics for verification need to capture the notion of permission ownership and transfer. One typical practice is the use of rational numbers in (0, 1] as permissions in which 1 is the full permission and the rest are fractional permissions. Rational permissions are not a good fit for separation logic because they remove the essential “disjointness” feature of the logic itself. We propose a general logic framework that supports permission reasoning in separation logic while preserving disjointness. Our framework is applicable to sophisticated verification tasks such as doing induction over the finiteness of the heap within the object logic or carrying out biabductive inference. We can also prove precision of recursive predicates within the object logic. We developed the ShareInfer tool to benchmark our techniques. We introduce “scaling separation algebras,” a compositional extension of separation algebras, to model our logic, and use them to construct a concrete model. © The Author(s) 2018.
dc.publisherSpringer Verlag
dc.sourceUnpaywall 20200831
dc.subjectAlgebra
dc.subjectComputer programming
dc.subjectFormal logic
dc.subjectSeparation
dc.subjectCommon resources
dc.subjectConcurrent programming
dc.subjectFractional permissions
dc.subjectLogical reasoning
dc.subjectRational numbers
dc.subjectResource sharing
dc.subjectSeparation logic
dc.subjectVerification task
dc.subjectComputer circuits
dc.typeConference Paper
dc.contributor.departmentYALE-NUS COLLEGE
dc.description.doi10.1007/978-3-319-89884-1_14
dc.description.sourcetitleLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.description.volume10801 LNCS
dc.description.page385-414
dc.published.statePublished
Appears in Collections:Staff Publications
Elements

Show simple item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
10_1007_978-3-319-89884-1_14.pdf1.03 MBAdobe PDF

OPEN

NoneView/Download

SCOPUSTM   
Citations

6
checked on Dec 5, 2022

Page view(s)

171
checked on Dec 1, 2022

Google ScholarTM

Check

Altmetric


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