Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Runtime Checking for Separation Logic
 
conference paper

Runtime Checking for Separation Logic

Nguyen, Huu Hai
•
Kuncak, Viktor  orcid-logo
•
Chin, Wei Ngan
2008
Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)

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.

  • Files
  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-540-78163-9_19
Author(s)
Nguyen, Huu Hai
Kuncak, Viktor  orcid-logo
Chin, Wei Ngan
Date Issued

2008

Publisher

Springer

Published in
Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
Series title/Series vol.

LNCS; 4905

Start page

203

End page

217

Subjects

run-time checking

•

separation logic

•

verification

•

contracts

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Event nameEvent placeEvent date
9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)

San Francisco, USA

January 7-9, 2008

Available on Infoscience
December 4, 2010
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/61906
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés