Skip to Main content Skip to Navigation
Journal articles

A linear concurrent constraint approach for the automatic verification of access permissions

Abstract : A recent trend in object oriented programming languages is the use Access Permissions (AP) as abstraction to control concurrent exe- cutions. AP define a protocol specifying how different references can access the mutable state of objects. Although AP simplify the task of writing concurrent code, an unsystematic use of permissions in the program can lead to subtle problems. This paper presents a Linear Concurrent Constraint (lcc) approach to verify AP an- notated programs. We model AP as constraints (i.e., formulas in logic) in an underlying constraint system, and we use entailment of constraints to faithfully model the flow of AP in the program. We verify relevant properties about programs by taking advantage of the declarative interpretation of lcc agents as formulas in lin- ear logic. Properties include deadlock detection, program correct- ness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. We show that those properties are decidable and we present a complexity analysis of finding such proofs. We implemented our verification and analysis approach as the Alcove tool, which is available on-line.
Document type :
Journal articles
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Catuscia Palamidessi Connect in order to contact the contributor
Submitted on : Sunday, November 4, 2012 - 11:55:44 PM
Last modification on : Monday, November 22, 2021 - 8:42:02 AM
Long-term archiving on: : Saturday, December 17, 2016 - 7:14:29 AM


Files produced by the author(s)



Carlos Olarte, Camilo Rueda, Elaine Pimentel, Nestor Cataño. A linear concurrent constraint approach for the automatic verification of access permissions. Proceedings of the 14th symposium on Principles and practice of declarative programming, ACM, 2012, pp.207-216. ⟨10.1145/2370776.2370802⟩. ⟨hal-00748141⟩



Record views


Files downloads