Paper Info
Title
Step-Indexed Kripke Model of Separation Logic for Storable Locks
Abstract
We present a version of separation logic for modular reasoning about concurrent programs with dynamically allocated storable locks and dynamic thread creation. The assertions of the program logic are modelled by a Kripke model over a recursively de. ned set of worlds and the program logic is proved sound through a Kripke relation to the standard operational semantics. This constitutes an elegant solution to the circularity issue arising from lock resource invariants depending on worlds containing lock resource invariants.
Year
DOI
Venue
2011
10.1016/j.entcs.2011.09.018
Electr. Notes Theor. Comput. Sci.
Keywords
DocType
Volume
separation logic,step-indexed kripke model,circularity issue,kripke model,lock resource,concurrent program,kripke relation,dynamic thread creation,storable lock,storable locks,program logic,lock resource invariants,concurrency,operational semantics,indexation,semantics
Journal
276,
ISSN
Citations 
PageRank 
1571-0661
9
0.58
References 
Authors
8
3
Name
Order
Citations
PageRank
Alexandre Buisse1372.74
Lars Birkedal2148196.84
Kristian Støvring3646.91