{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:12:50Z","timestamp":1725549170062},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120282"},{"type":"electronic","value":"9783642120299"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12029-9_19","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:56:48Z","timestamp":1267991808000},"page":"263-277","source":"Crossref","is-referenced-by-count":7,"title":["Shape Refinement through Explicit Heap Analysis"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gr\u00e9gory","family":"Th\u00e9oduloz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","first-page":"1","volume-title":"Proc. POPL","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1\u20133. ACM, New York (2002)"},{"key":"19_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1390630.1390634","volume-title":"Proc. ISSTA","author":"N. Beckman","year":"2008","unstructured":"Beckman, N., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Proc. ISSTA, pp. 3\u201314. ACM, New York (2008)"},{"issue":"5-6","key":"19_CR3","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer\u00a09(5-6), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 532\u2013546. Springer, Heidelberg (2006)"},{"key":"19_CR5","first-page":"29","volume-title":"Proc. ASE","author":"D. Beyer","year":"2008","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE, pp. 29\u201338. IEEE, Los Alamitos (2008)"},{"issue":"6","key":"19_CR6","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng.\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"5","key":"19_CR7","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"19_CR8","first-page":"117","volume-title":"Proc. FSE","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: A new algorithm for property checking. In: Proc. FSE, pp. 117\u2013127. ACM, New York (2006)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Rajamani, S.K.: Counterexample-driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-642-00768-2_24","volume-title":"ACAS 2009","author":"A. Gupta","year":"2009","unstructured":"Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) ACAS 2009. LNCS, vol.\u00a05505, pp. 262\u2013276. Springer, Heidelberg (2009)"},{"key":"19_CR11","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"Proc. POPL","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL, pp. 232\u2013244. ACM Press, New York (2004)"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-540-30482-1_23","volume-title":"Formal Methods and Software Engineering","author":"D. Kr\u00f6ning","year":"2004","unstructured":"Kr\u00f6ning, D., Groce, A., Clarke, E.M.: Counterexample-guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 224\u2013238. Springer, Heidelberg (2004)"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T.W., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"19_CR15","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/199448.199462","volume-title":"Proc. POPL","author":"T.W. Reps","year":"1995","unstructured":"Reps, T.W., Horwitz, S., Sagiv, M.: Precise interprocedural data-flow analysis via graph reachability. In: Proc. POPL, pp. 49\u201361. ACM, New York (1995)"},{"key":"19_CR16","unstructured":"Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural functional shape analysis using local heaps. Technical Report TAU-CS-26\/04, Tel-Aviv University (2004)"},{"issue":"3","key":"19_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"19_CR18","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/1146238.1146255","volume-title":"Proc. ISSTA","author":"G. Yorsh","year":"2006","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: Better together! In: Proc. ISSTA, pp. 145\u2013156. ACM, New York (2006)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12029-9_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T15:56:43Z","timestamp":1685462203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12029-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120282","9783642120299"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12029-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}