{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:06Z","timestamp":1775868546485,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662491218","type":"print"},{"value":"9783662491225","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_3","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"65-84","source":"Crossref","is-referenced-by-count":7,"title":["Predicate Abstraction for Linked Data Structures"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Bakst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"3_CR1","unstructured":"https:\/\/github.com\/UCSD-PL\/nano-js\/tree\/vmcai_2016\/tests\/eval"},{"issue":"4","key":"3_CR2","first-page":"397","volume":"77","author":"A Ahmed","year":"2007","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L\n                      \n                        \n                      \n                      $$^3$$\n                    : a linear language with locations. Fundam. Inf. 77(4), 397\u2013449 (2007)","journal-title":"Fundam. Inf."},{"key":"3_CR3","unstructured":"Bakst, A., Jhala, R.: Predicate abstraction for linked data structures. \n                      http:\/\/arxiv.org\/abs\/1505.02298"},{"key":"3_CR4","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. 4111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"3_CR5","first-page":"5","volume":"254","author":"M Botin\u010dan","year":"2009","unstructured":"Botin\u010dan, M., Parkinson, M., Schulte, W.: Separation logic verification of c programs with an smt solver. ENTCS 254, 5\u201323 (2009)","journal-title":"ENTCS"},{"key":"3_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. 7561, pp. 167\u2013182. Springer, Heidelberg (2012)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Chang, B.E., Rival, X.: Relational inductive shape analysis. In: POPL (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Functional translation of a calculus of capabilities. In: Hook, J., Thiemann, P. (eds.), Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), pp. 213\u2013224. ACM (2008)","DOI":"10.1145\/1411204.1411235"},{"issue":"9","key":"3_CR9","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., 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_CR10","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI. ACM (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"3_CR11","unstructured":"Chu, D.-H., Jaffar, J., Trinh, M.-T.: Automatic induction proofs of data-structures in imperative programs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15\u201317, 2015, pP. 457\u2013466 (2015)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"issue":"3","key":"3_CR13","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"3_CR14","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)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"3_CR16","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)"},{"key":"3_CR17","unstructured":"Heule, S., Kassios, I.T., M\u00fcller, P., Summers, A.J.: Verification condition generation for permission logics with abstract predicates and abstraction functions"},{"issue":"5","key":"3_CR18","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"P G\u00e9rard","year":"1997","unstructured":"G\u00e9rard, P.: Huet. The zipper. J. Funct. Program. 7(5), 549\u2013554 (1997)","journal-title":"Huet. The zipper. J. Funct. Program."},{"key":"3_CR19","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_CR20","doi-asserted-by":"crossref","unstructured":"Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: PLDI (2009)","DOI":"10.1145\/1542476.1542510"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"static analysis","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: a system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280\u2013301. Springer, Heidelberg (2000)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-70545-1_41","volume-title":"Computer Aided Verification","author":"S Magill","year":"2008","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: THOR: a tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 428\u2013432. Springer, Heidelberg (2008)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: reasoning with the awkward squad. In: ICFP (2008)","DOI":"10.1145\/1411204.1411237"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Nystrom, N., Saraswat, V., Palsberg, J., Grothoff, C.: Constrained types for object-oriented languages. In: OOPSLA. ACM (2008)","DOI":"10.1145\/1449764.1449800"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in c using separation logic. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 46. ACM (2014)","DOI":"10.1145\/2594291.2594325"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic+ superposition calculus = heap theorem prover. In: PLDI (2011)","DOI":"10.1145\/1993498.1993563"},{"key":"3_CR28","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. 8044, pp. 773\u2013789. Springer, Heidelberg (2013)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Pottier, F., Protzenko, J.: Programming with permissions in mezzo. In: ICFP (2013)","DOI":"10.1145\/2500365.2500598"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI (2013)","DOI":"10.1145\/2491956.2462169"},{"key":"3_CR31","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI (2008)","DOI":"10.1145\/1375581.1375602"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Rondon, P., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: POPL (2010)","DOI":"10.1145\/1706299.1706316"},{"key":"3_CR34","unstructured":"Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. In: 29th European Conference on Object-Oriented Programming, ECOOP 2015, July 5\u201310, 2015, Prague, Czech Republic, pp. 614\u2013638 (2015)"},{"issue":"10","key":"3_CR35","doi-asserted-by":"crossref","first-page":"713","DOI":"10.1145\/2076021.2048122","volume":"46","author":"Joshua Sunshine","year":"2011","unstructured":"Sunshine, J., Naden, K., Stork, S., Aldrich, J., Tanter, E.: First-class state change in plaid. In: OOPSLA (2011)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"3_CR36","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1145\/1707801.1706325","volume":"45","author":"Philippe Suter","year":"2010","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL (2010)","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-37036-6_13","volume-title":"Programming Languages and Systems","author":"N Vazou","year":"2013","unstructured":"Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209\u2013228. Springer, Heidelberg (2013)"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Walker, D., Morrisett, J.G.; Alias types for recursive data structures. In: Types in Compilation (2000)","DOI":"10.1007\/3-540-45332-6_7"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL (1999)","DOI":"10.1145\/292540.292560"},{"key":"3_CR40","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)"},{"issue":"6","key":"3_CR41","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/1379022.1375624","volume":"43","author":"Karen Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: PLDI, pp. 349\u2013361 (2008)","journal-title":"ACM SIGPLAN Notices"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T04:34:40Z","timestamp":1559363680000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}