{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,19]],"date-time":"2026-09-19T15:48:13Z","timestamp":1789832893888,"version":"4.0.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319229683","type":"print"},{"value":"9783319229690","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22969-0_3","type":"book-chapter","created":{"date-parts":[[2015,8,20]],"date-time":"2015-08-20T08:51:42Z","timestamp":1440060702000},"page":"37-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Learning Assertions to Verify Linked-List Programs"],"prefix":"10.1007","author":[{"given":"Jan Tobias","family":"M\u00fchlberg","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David H.","family":"White","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mike","family":"Dodds","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,8,21]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. In: POPL 2002, pp. 4\u201316. ACM (2002)","DOI":"10.1145\/565816.503275"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"3_CR3","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. 6806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"3_CR4","unstructured":"The Boa webserver. http:\/\/www.boa.org\/. Accessed 2015\u201306-09"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL 2005, pp. 259\u2013270. ACM (2005)","DOI":"10.1145\/1047659.1040327"},{"issue":"1","key":"3_CR6","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1145\/1594834.1480917","volume":"44","author":"C Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. SIGPLAN Not. 44(1), 289\u2013300 (2009)","journal-title":"SIGPLAN Not."},{"issue":"9","key":"3_CR7","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA 2008, pp. 213\u2013226. ACM (2008)","DOI":"10.1145\/1449955.1449782"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI 2005, pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: PLDI 2007, pp. 256\u2013265. ACM (2007)","DOI":"10.1145\/1273442.1250764"},{"issue":"1\u20132","key":"3_CR11","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10994-013-5419-7","volume":"96","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: Learning register automata: from languages to program structures. Mach. Learn. 96(1\u20132), 65\u201398 (2014)","journal-title":"Mach. Learn."},{"key":"3_CR12","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. 6617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Jung, C., Clark, N.: DDT: design and evaluation of a dynamic program analysis for optimizing data structure usage. In: MICRO 2009, pp. 56\u201366. ACM (2009)","DOI":"10.1145\/1669112.1669122"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis transformation. In: CGO 2004, pp. 75\u201386. IEEE (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"3_CR15","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":"PW O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.scico.2013.01.006","volume":"82","author":"P Philippaerts","year":"2014","unstructured":"Philippaerts, P., M\u00fchlberg, J.T., Penninckx, W., Smans, J., Jacobs, B., Piessens, F.: Software verification with VeriFast: industrial case studies. Sci. Comput. Program. 82, 77\u201397 (2014)","journal-title":"Sci. Comput. Program."},{"key":"3_CR17","unstructured":"The Redis key-value store. http:\/\/www.redis.io\/. Accessed 2015\u201306-09"},{"issue":"3","key":"3_CR18","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-21461-5_21","volume-title":"Formal Techniques for Distributed Systems","author":"F Vogels","year":"2011","unstructured":"Vogels, F., Jacobs, B., Piessens, F., Smans, J.: Annotation inference for separation logic based verifiers. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 319\u2013333. Springer, Heidelberg (2011)"},{"key":"3_CR20","volume-title":"Data Structures and Algorithm Analysis in C","author":"MA Weiss","year":"1997","unstructured":"Weiss, M.A.: Data Structures and Algorithm Analysis in C, 2nd edn. Addison-Wesley, Boston (1997)","edition":"2"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-36742-7_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DH White","year":"2013","unstructured":"White, D.H., L\u00fcttgen, G.: Identifying dynamic data structures by learning evolving patterns in memory. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 354\u2013369. Springer, Heidelberg (2013)"},{"key":"3_CR22","volume-title":"C von A bis Z","author":"J Wolf","year":"2009","unstructured":"Wolf, J.: C von A bis Z. Galileo Computing, Germany (2009)"},{"key":"3_CR23","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. 5123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22969-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T02:54:14Z","timestamp":1748573654000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22969-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319229683","9783319229690"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22969-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"21 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}