{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:58:28Z","timestamp":1768006708250,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540883869","type":"print"},{"value":"9783540883876","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-88387-6_10","type":"book-chapter","created":{"date-parts":[[2008,10,10]],"date-time":"2008-10-10T01:42:45Z","timestamp":1223602965000},"page":"111-125","source":"Crossref","is-referenced-by-count":32,"title":["Loop Summarization Using Abstract Transformers"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Kroening","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aliaksei","family":"Tsitovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T.W. Reps","year":"2004","unstructured":"Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic Implementation of the Best Transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"key":"10_CR5","first-page":"105","volume":"25","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD\u00a025, 105\u2013127 (2004)","journal-title":"FMSD"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-73368-3_10","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.W.: Low-level library analysis and summarization. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 68\u201381. Springer, Heidelberg (2007)"},{"key":"10_CR7","volume-title":"Program Flow Analysis: theory and applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: theory and applications. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/1251535.1251543","volume-title":"PASTE","author":"A. Aiken","year":"2007","unstructured":"Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the Saturn project. In: PASTE, pp. 43\u201348. ACM, New York (2007)"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/1368088.1368118","volume-title":"ICSE","author":"D. Babic","year":"2008","unstructured":"Babic, D., Hu, A.J.: Calysto: scalable and precise extended static checking. In: ICSE, pp. 211\u2013220. ACM, New York (2008)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA, pp. 14\u201325 (2000)","DOI":"10.1145\/347324.383378"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"10_CR12","volume-title":"Model checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/11513988_5","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2005","unstructured":"Lahiri, S.K., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 24\u201338. Springer, Heidelberg (2005)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/11691372_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Kroening","year":"2006","unstructured":"Kroening, D., Sharygina, N.: Approximating predicate images for bit-vector logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 242\u2013256. Springer, Heidelberg (2006)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11817963_39","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2006","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 424\u2013437. Springer, Heidelberg (2006)"},{"key":"10_CR18","first-page":"69","volume-title":"FMCAD","author":"R. Cavada","year":"2007","unstructured":"Cavada, R., Cimatti, A., Franz\u00e9n, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing predicate abstractions by integrating BDDs and SMT solvers. In: FMCAD, pp. 69\u201376. IEEE, Los Alamitos (2007)"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1145\/322261.322273","volume":"28","author":"R.E. Tarjan","year":"1981","unstructured":"Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM\u00a028, 594\u2013614 (1981)","journal-title":"J. ACM"},{"key":"10_CR20","unstructured":"Ashcroft, E., Manna, Z.: The translation of \u2019go to\u2019 programs to \u2019while\u2019 programs, pp. 49\u201361 (1979)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Dor, N., Rodeh, M., Sagiv, S.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: PLDI, pp. 155\u2013167 (2003)","DOI":"10.1145\/781131.781149"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. In: SIGSOFT FSE, pp. 97\u2013106 (2004)","DOI":"10.1145\/1029894.1029911"},{"key":"10_CR23","first-page":"389","volume-title":"ASE 2007","author":"K. Ku","year":"2007","unstructured":"Ku, K., Hart, T.E., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: ASE 2007, pp. 389\u2013392. ACM Press, New York (2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88387-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,3]],"date-time":"2019-03-03T12:42:24Z","timestamp":1551616944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88387-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540883869","9783540883876"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88387-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}