{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:36Z","timestamp":1775790696167,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540781622","type":"print"},{"value":"9783540781639","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_19","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T10:30:06Z","timestamp":1204281006000},"page":"203-217","source":"Crossref","is-referenced-by-count":14,"title":["Runtime Checking for Separation Logic"],"prefix":"10.1007","author":[{"given":"Huu Hai","family":"Nguyen","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS 2004 (2004)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Berdine, J., et al.: Shape analysis for composite data structures. In: CAV 2007 (2007)","DOI":"10.1007\/978-3-540-73368-3_22"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO, pp. 115\u2013137 (2005)","DOI":"10.1007\/11804192_6"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_25","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"E. Bodden","year":"2007","unstructured":"Bodden, E., Hendren, L., Lhot\u00e1k, O.: A staged static program analysis to improve the performance of runtime monitoring. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, Springer, Heidelberg (2007)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., et al.: Footprint analysis: A shape analysis that discovers preconditions. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, Springer, Heidelberg (2007)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.: Computability and complexity results for a spatial assertion language for data structures. In: FSTTCS 2001 (2001)","DOI":"10.1007\/3-540-45294-X_10"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Cartwright, R., Fagan, M.: Soft typing. In: PLDI 1991, pp. 278\u2013292 (1991)","DOI":"10.1145\/113445.113469"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Chen, F., Ro\u015fu, G.: MOP: An Efficient and Generic Runtime Verification Framework. In: OOPSLA 2007 (2007)","DOI":"10.1145\/1297027.1297069"},{"key":"19_CR9","unstructured":"Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language. PhD thesis, Iowa State University (April 2003)"},{"issue":"3","key":"19_CR10","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/1127878.1127900","volume":"31","author":"L.A. Clarke","year":"2006","unstructured":"Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. SIGSOFT Softw. Eng. Notes\u00a031(3), 25\u201337 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Demsky, B., et al.: Efficient specification-assisted error localization. In: Second International Workshop on Dynamic Analysis (2004)","DOI":"10.1049\/ic:20040301"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: ICFP (2002)","DOI":"10.1145\/581478.581484"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI 2007 (2007)","DOI":"10.1145\/1250734.1250764"},{"key":"19_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"J. Guttag","year":"1993","unstructured":"Guttag, J., Horning, J.: Larch: Languages and Tools for Formal Specification. Springer, Heidelberg (1993)"},{"key":"19_CR15","volume-title":"Descriptive Complexity","author":"N. Immerman","year":"1998","unstructured":"Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1998)"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM POPL 2001 (2001)","DOI":"10.1145\/360204.375719"},{"key":"19_CR17","unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)"},{"key":"19_CR18","unstructured":"Kuncak, V., Rinard, M.: On spatial conjunction as second-order logic. Technical Report 970, MIT CSAIL (October 2004)"},{"key":"19_CR19","unstructured":"Lev-Ami, T.: TVLA: A framework for Kleene based logic static analyses. Master\u2019s thesis, Tel-Aviv University, Israel (2000)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., et al.: Putting static analysis to work for verification: A case study. In: Int. Symp. Software Testing and Analysis (2000)","DOI":"10.1145\/347324.348031"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Lo, D., Khoo, S.-C., Liu, C.: Efficient mining of iterative patterns for software specification discovery. In: SIGKDD 2007 (2007)","DOI":"10.1145\/1281192.1281243"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Nguyen, H.H., et al.: Automated verification of shape and size properties via separation logic. In: VMCAI 2007 (2007)","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"19_CR23","unstructured":"Nguyen, H.H., Kuncak, V., Chin, W.-N.: Runtime Checking for Separation Logic. EPFL Technical Report LARA-REPORT-2007-003 (2007)"},{"key":"19_CR24","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/571157.571169","volume-title":"PPDP","author":"D. Overton","year":"2002","unstructured":"Overton, D., Somogyi, Z., Stuckey, P.J.: Constraint-based mode analysis of mercury. In: PPDP, pp. 109\u2013120. ACM Press, New York (2002)"},{"key":"19_CR25","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1173706.1173723","volume-title":"GPCE","author":"F. Perry","year":"2006","unstructured":"Perry, F., Jia, L., Walker, D.: Expressing heap-shape contracts in linear logic. In: GPCE, pp. 101\u2013110. ACM Press, New York (2006)"},{"key":"19_CR26","unstructured":"Reineke, J.: Shape analysis of sets. Master\u2019s thesis, Universit\u00e4t des Saarlandes, Germany (June 2005)"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Shankar, A., Bodik, R.: Ditto: Automatic incrementalization of data structure invariant checks. In: PLDI 2007 (2007)","DOI":"10.1145\/1250734.1250770"},{"key":"19_CR29","unstructured":"Somogyi, Z.: A system of precise modes for logic programs. In: ICLP 1987 (1987)"},{"key":"19_CR30","unstructured":"Wies, T., et al.: Field constraint analysis. In: VMCAI 2006 (2006)"},{"key":"19_CR31","unstructured":"Zee, K., et al.: Runtime checking for program verification systems. In: RV (collocated with AOSD) (2007)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,28]],"date-time":"2025-01-28T21:01:51Z","timestamp":1738098111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_19","relation":{},"subject":[]}}