{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:16:14Z","timestamp":1760044574418,"version":"3.41.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319667058"},{"type":"electronic","value":"9783319667065"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66706-5_4","type":"book-chapter","created":{"date-parts":[[2017,8,18]],"date-time":"2017-08-18T04:13:26Z","timestamp":1503029606000},"page":"66-87","source":"Crossref","is-referenced-by-count":8,"title":["Learning Shape Analysis"],"prefix":"10.1007","author":[{"given":"Marc","family":"Brockschmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuxin","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pushmeet","family":"Kohli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siddharth","family":"Krishna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Tarlow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,19]]},"reference":[{"issue":"4","key":"4_CR1","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/s00236-015-0235-0","volume":"53","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Hol\u00edk, L., Jonsson, B., Leng\u00e1l, O., Trinh, C.Q., Vojnar, T.: Verification of heap manipulating programs with ordered data by extended forest automata. Acta Inf. 53(4), 357\u2013385 (2016)","journal-title":"Acta Inf."},{"unstructured":"Allamanis, M., Tarlow, D., Gordon, A.D., Wei, Y.: Bimodal modelling of source code and natural language. In: ICML 2015, pp. 2123\u20132132 (2015)","key":"4_CR2"},{"doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: POPL 2011, pp. 599\u2013610 (2011)","key":"4_CR3","DOI":"10.1145\/1926385.1926454"},{"doi-asserted-by":"crossref","unstructured":"Bakir, G.H., Hofmann, T., Sch\u00f6lkopf, B., Smola, A.J., Taskar, B., Vishwanathan, S.V.N.: Predicting Structured Data. MIT Press (2007)","key":"4_CR4","DOI":"10.7551\/mitpress\/7443.001.0001"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178\u2013192. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73368-3_22"},{"doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.: Implementing TLS with verified cryptographic security. In: SP 2013, pp. 445\u2013459 (2013)","key":"4_CR6","DOI":"10.1109\/SP.2013.37"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-27940-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 1\u201322. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-27940-9_1"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-18275-4_7"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-22438-6_12","volume-title":"Automated Deduction \u2013 CADE-23","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131\u2013146. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_12"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-319-10936-7_5","volume-title":"Static Analysis","author":"J Brotherston","year":"2014","unstructured":"Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 68\u201384. Springer, Cham (2014). doi: 10.1007\/978-3-319-10936-7_5"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-35182-2_25","volume-title":"Programming Languages and Systems","author":"J Brotherston","year":"2012","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350\u2013367. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-35182-2_25"},{"issue":"6","key":"4_CR12","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)","journal-title":"J. ACM"},{"key":"4_CR13","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. 6806, pp. 372\u2013378. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_29"},{"issue":"1\u20133","key":"4_CR14","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_5"},{"doi-asserted-by":"crossref","unstructured":"Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: POPL 2016, pp. 499\u2013512 (2016)","key":"4_CR16","DOI":"10.1145\/2837614.2837664"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/11823230_16","volume-title":"Static Analysis","author":"A Gotsman","year":"2006","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240\u2013260. Springer, Heidelberg (2006). doi: 10.1007\/11823230_16"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"790","DOI":"10.1007\/978-3-642-39799-8_55","volume-title":"Computer Aided Verification","author":"C Haase","year":"2013","unstructured":"Haase, C., Ishtiaq, S., Ouaknine, J., Parkinson, M.J.: SeLoger: a tool for graph-based reasoning in separation logic. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 790\u2013795. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_55"},{"doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: IronFleet: proving practical distributed systems correct. In: SOSP 2015, pp. 1\u201317 (2015)","key":"4_CR19","DOI":"10.1145\/2815400.2815428"},{"key":"4_CR20","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. 8044, pp. 756\u2013772. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_53"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-08867-9_3","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2014","unstructured":"Itzhaky, S., Bj\u00f8rner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 35\u201351. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_3"},{"issue":"4","key":"4_CR22","first-page":"892","volume":"25","author":"Y Jung","year":"2015","unstructured":"Jung, Y., Kong, S., David, C., Wang, B., Yi, K.: Automatically inferring loop invariants via algorithmic learning. MSCS 25(4), 892\u2013915 (2015)","journal-title":"MSCS"},{"issue":"4\u20135","key":"4_CR23","first-page":"529","volume":"22","author":"AJ Kennedy","year":"2012","unstructured":"Kennedy, A.J., Vytiniotis, D.: Every bit counts: the binary representation of typed data and programs. JFP 22(4\u20135), 529\u2013573 (2012)","journal-title":"JFP"},{"issue":"1","key":"4_CR24","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. TOCS 32(1), 2 (2014)","journal-title":"TOCS"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-319-08867-9_4","volume-title":"Computer Aided Verification","author":"QL Le","year":"2014","unstructured":"Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52\u201368. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_4"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-41528-4_21","volume-title":"Computer Aided Verification","author":"QL Le","year":"2016","unstructured":"Le, Q.L., Sun, J., Chin, W.-N.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 382\u2013404. Springer, Cham (2016). doi: 10.1007\/978-3-319-41528-4_21"},{"issue":"7","key":"4_CR27","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107\u2013115 (2009)","journal-title":"CACM"},{"unstructured":"Li, Y., Tarlow, D., Brockschmidt, M., Zemel, R.: Gated graph sequence neural networks. In: ICLR 2016 (2016)","key":"4_CR28"},{"doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M., Lee, P., Tsay, Y.: Automatic numeric abstractions for heap-manipulating programs. In: POPL 2010, pp. 211\u2013222 (2010)","key":"4_CR29","DOI":"10.1145\/1706299.1706326"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). doi: 10.1007\/11817963_14"},{"issue":"11","key":"4_CR31","doi-asserted-by":"crossref","first-page":"1184","DOI":"10.1016\/j.jsc.2010.06.004","volume":"45","author":"Y Moy","year":"2010","unstructured":"Moy, Y., March\u00e9, C.: Modular inference of subprogram contracts for safety checking. J. Symb. Comput. 45(11), 1184\u20131211 (2010)","journal-title":"J. Symb. Comput."},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-22969-0_3","volume-title":"Software Engineering and Formal Methods","author":"JT M\u00fchlberg","year":"2015","unstructured":"M\u00fchlberg, J.T., White, D.H., Dodds, M., L\u00fcttgen, G., Piessens, F.: Learning assertions to verify linked-list programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 37\u201352. Springer, Cham (2015). doi: 10.1007\/978-3-319-22969-0_3"},{"key":"4_CR33","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. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44802-0_1"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-319-03542-0_7","volume-title":"Programming Languages and Systems","author":"JA Navarro P\u00e9rez","year":"2013","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 90\u2013106. Springer, Cham (2013). doi: 10.1007\/978-3-319-03542-0_7"},{"doi-asserted-by":"publisher","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124\u2013139. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_9","key":"4_CR35","DOI":"10.1007\/978-3-642-54862-8_9"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374 (2002)","key":"4_CR36","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"4_CR37","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217\u2013298 (2002)","journal-title":"TOPLAS"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-319-08867-9_6","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2014","unstructured":"Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 88\u2013105. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_6"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-642-37036-6_31","volume-title":"Programming Languages and Systems","author":"R Sharma","year":"2013","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574\u2013592. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37036-6_31"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-38856-9_21","volume-title":"Static Analysis","author":"R Sharma","year":"2013","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Verification as learning geometric concepts. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 388\u2013411. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38856-9_21"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-31424-7_11","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2012","unstructured":"Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 71\u201387. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_11"},{"doi-asserted-by":"crossref","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: better together! In: ISSTA 2006, pp. 145\u2013156 (2006)","key":"4_CR42","DOI":"10.1145\/1146238.1146255"},{"doi-asserted-by":"crossref","unstructured":"Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: PLDI 2016 (2016)","key":"4_CR43","DOI":"10.1145\/2908080.2908125"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66706-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:21:02Z","timestamp":1750807262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66706-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319667058","9783319667065"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66706-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}