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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS 2004 (2004)
Berdine, J., et al.: Shape analysis for composite data structures. In: CAV 2007 (2007)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO, pp. 115–137 (2005)
Bodden, E., Hendren, L., Lhoták, O.: A staged static program analysis to improve the performance of runtime monitoring. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, Springer, Heidelberg (2007)
Calcagno, C., et al.: Footprint analysis: A shape analysis that discovers preconditions. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, Springer, Heidelberg (2007)
Calcagno, C., Yang, H., O’Hearn, P.: Computability and complexity results for a spatial assertion language for data structures. In: FSTTCS 2001 (2001)
Cartwright, R., Fagan, M.: Soft typing. In: PLDI 1991, pp. 278–292 (1991)
Chen, F., Roşu, G.: MOP: An Efficient and Generic Runtime Verification Framework. In: OOPSLA 2007 (2007)
Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Iowa State University (April 2003)
Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes 31(3), 25–37 (2006)
Demsky, B., et al.: Efficient specification-assisted error localization. In: Second International Workshop on Dynamic Analysis (2004)
Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: ICFP (2002)
Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI 2007 (2007)
Guttag, J., Horning, J.: Larch: Languages and Tools for Formal Specification. Springer, Heidelberg (1993)
Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1998)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM POPL 2001 (2001)
Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)
Kuncak, V., Rinard, M.: On spatial conjunction as second-order logic. Technical Report 970, MIT CSAIL (October 2004)
Lev-Ami, T.: TVLA: A framework for Kleene based logic static analyses. Master’s thesis, Tel-Aviv University, Israel (2000)
Lev-Ami, T., et al.: Putting static analysis to work for verification: A case study. In: Int. Symp. Software Testing and Analysis (2000)
Lo, D., Khoo, S.-C., Liu, C.: Efficient mining of iterative patterns for software specification discovery. In: SIGKDD 2007 (2007)
Nguyen, H.H., et al.: Automated verification of shape and size properties via separation logic. In: VMCAI 2007 (2007)
Nguyen, H.H., Kuncak, V., Chin, W.-N.: Runtime Checking for Separation Logic. EPFL Technical Report LARA-REPORT-2007-003 (2007)
Overton, D., Somogyi, Z., Stuckey, P.J.: Constraint-based mode analysis of mercury. In: PPDP, pp. 109–120. ACM Press, New York (2002)
Perry, F., Jia, L., Walker, D.: Expressing heap-shape contracts in linear logic. In: GPCE, pp. 101–110. ACM Press, New York (2006)
Reineke, J.: Shape analysis of sets. Master’s thesis, Universität des Saarlandes, Germany (June 2005)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74 (2002)
Shankar, A., Bodik, R.: Ditto: Automatic incrementalization of data structure invariant checks. In: PLDI 2007 (2007)
Somogyi, Z.: A system of precise modes for logic programs. In: ICLP 1987 (1987)
Wies, T., et al.: Field constraint analysis. In: VMCAI 2006 (2006)
Zee, K., et al.: Runtime checking for program verification systems. In: RV (collocated with AOSD) (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nguyen, H.H., Kuncak, V., Chin, WN. (2008). Runtime Checking for Separation Logic. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2008. Lecture Notes in Computer Science, vol 4905. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78163-9_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-78163-9_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78162-2
Online ISBN: 978-3-540-78163-9
eBook Packages: Computer ScienceComputer Science (R0)