000161471 001__ 161471
000161471 005__ 20190316235006.0
000161471 0247_ $$2doi$$a10.1007/978-3-540-78163-9_19
000161471 037__ $$aCONF
000161471 245__ $$aRuntime Checking for Separation Logic
000161471 269__ $$a2008
000161471 260__ $$bSpringer$$c2008
000161471 336__ $$aConference Papers
000161471 490__ $$aLNCS$$v4905
000161471 520__ $$aSeparation 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.
000161471 6531_ $$arun-time checking
000161471 6531_ $$aseparation logic
000161471 6531_ $$averification
000161471 6531_ $$acontracts
000161471 700__ $$aNguyen, Huu Hai
000161471 700__ $$0240031$$g177241$$aKuncak, Viktor
000161471 700__ $$aChin, Wei Ngan
000161471 7112_ $$dJanuary 7-9, 2008$$cSan Francisco, USA$$a9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
000161471 773__ $$tProceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)$$q203-217
000161471 8564_ $$uhttps://infoscience.epfl.ch/record/161471/files/NguyenETAL08RuntimeCheckingSeparationLogic.pdf$$zn/a$$s220701$$yPreprint
000161471 909C0 $$xU11739$$0252019$$pLARA
000161471 909CO $$qGLOBAL_SET$$pconf$$ooai:infoscience.tind.io:161471$$pIC
000161471 917Z8 $$x177241
000161471 937__ $$aEPFL-CONF-161471
000161471 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000161471 980__ $$aCONF