Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-540-78163-9_19
Title: Runtime checking for separation logic
Authors: Nguyen, H.H.
Kuncak, V.
Chin, W.-N. 
Issue Date: 2008
Source: Nguyen, H.H.,Kuncak, V.,Chin, W.-N. (2008). Runtime checking for separation logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4905 LNCS : 203-217. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-540-78163-9_19
Abstract: Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static analysis techniques. Checking data structure specifications during program execution is an alternative to static verification: it can enforce the sophisticated specifications for which static verification fails, and it can help debug incorrect specifications and code by detecting concrete counterexamples to their validity. This paper presents Separation Logic Invariant ChecKer (SLICK), a runtime checker for separation logic specifications. We show that, although the recursive style of separation logic predicates is well suited for runtime execution, the implicit footprint and existential quantification make efficient runtime checking challenging. To address these challenges we introduce a coloring technique for efficiently checking method footprints and describe techniques for inferring values of existentially quantified variables. We have implemented our runtime checker in the context of a tool for enforcing specifications of Java programs. Our experience suggests that our runtime checker is a useful companion to a static verifier for separation logic specifications. © 2008 Springer-Verlag Berlin Heidelberg.
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/41684
ISBN: 3540781625
ISSN: 03029743
DOI: 10.1007/978-3-540-78163-9_19
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

8
checked on Dec 13, 2017

Page view(s)

42
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


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