{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:58Z","timestamp":1775868538282,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548611","type":"print"},{"value":"9783642548628","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_9","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:33:34Z","timestamp":1395394414000},"page":"124-139","source":"Crossref","is-referenced-by-count":48,"title":["GRASShopper"],"prefix":"10.1007","author":[{"given":"Ruzica","family":"Piskac","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[]},{"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-75560-9_4","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Abadi","year":"2007","unstructured":"Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 17\u201331. Springer, Heidelberg (2007)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory Safety for Systems-Level Code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2009.09.057","volume":"254","author":"M. Botincan","year":"2009","unstructured":"Botincan, M., Parkinson, M.J., Schulte, W.: Separation logic verification of C programs with an SMT solver. Electr. Notes Theor. Comput. Sci.\u00a0254, 5\u201323 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-33386-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 167\u2013182. Springer, Heidelberg (2012)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B. Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 235\u2013249. Springer, Heidelberg (2011)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-22110-1_29","volume-title":"Computer Aided Verification","author":"K. Dudka","year":"2011","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: A practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 372\u2013378. Springer, Heidelberg (2011)"},{"key":"9_CR10","unstructured":"GRASShopper tool wep page, \n                    \n                      http:\/\/cs.nyu.edu\/wies\/software\/grasshopper\n                    \n                    \n                   (last accessed: October 2013)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer Science Logic","author":"N. Immerman","year":"2004","unstructured":"Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive-closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-38574-2_2","volume-title":"Automated Deduction \u2013 CADE-24","author":"R. Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 21\u201338. Springer, Heidelberg (2013)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1007\/978-3-642-39799-8_53","volume-title":"Computer Aided Verification","author":"S. Itzhaky","year":"2013","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 756\u2013772. Springer, Heidelberg (2013)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Lahav, O., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Modular reasoning on unique heap paths via effectively propositional formulas. In: POPL (2014)","DOI":"10.1145\/2535838.2535854"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: POPL (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"9_CR17","series-title":"LNCS","first-page":"195","volume-title":"FOSAD","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol.\u00a05705, pp. 195\u2013222. Springer, Heidelberg (2009)"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Logical Methods in Computer Science\u00a08(3) (2012)","DOI":"10.2168\/LMCS-8(3:1)2012"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"P\u00e9rez, J.A.N., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI, pp. 556\u2013566. ACM (2011)","DOI":"10.1145\/1993316.1993563"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating Separation Logic Using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 773\u2013789. Springer, Heidelberg (2013)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI, pp. 231\u2013242 (2013)","DOI":"10.1145\/2499370.2462169"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-03013-0_8","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"J. Smans","year":"2009","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol.\u00a05653, pp. 148\u2013172. Springer, Heidelberg (2009)"},{"key":"9_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: POPL. ACM (2013)","DOI":"10.1145\/2429069.2429132"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T07:58:18Z","timestamp":1558857498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_9"}},"subtitle":["Complete Heap Verification with Mixed Specifications"],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}