Runtime Checking for Separation Logic

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.

Citation

Huu Hai Nguyen, Viktor Kuncak, and Wei Ngan Chin. Runtime checking for separation logic. In 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, 2008.

BibTex Entry

@inproceedings{NguyenETAL08RuntimeCheckingSeparationLogic,
  author = {Huu Hai Nguyen and Viktor Kuncak and Wei Ngan Chin},
  title = {Runtime Checking for Separation Logic},
  booktitle = {9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  series = {LNCS},
  year = 2008,
  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.
 }
}