{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:49:27Z","timestamp":1725572967751},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_16","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"152-165","source":"Crossref","is-referenced-by-count":21,"title":["Counterexamples with Loops for Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Kroening","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"16_CR3","unstructured":"Ball, T., Rajamani, S.: Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research (2000)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume-title":"Integrated Formal Methods","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"16_CR6","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R. Kurshan","year":"1995","unstructured":"Kurshan, R.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1995)"},{"key":"16_CR7","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM Press, New York (2002)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/11537328_9","volume-title":"Model Checking Software","author":"B. Cook","year":"2005","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Symbolic model checking for asynchronous Boolean programs. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 75\u201390. Springer, Heidelberg (2005)"},{"key":"16_CR9","unstructured":"Ball, T., Rajamani, S.: Generating Abstract Explanations of Spurious Counterexamples in C Programs. Technical Report MSR-TR-2002-09, Microsoft Research, Redmond (2002)"},{"key":"16_CR10","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/1065010.1065016","volume-title":"PLDI","author":"R. Jhala","year":"2005","unstructured":"Jhala, R., Majumdar, R.: Path slicing. In: PLDI, pp. 38\u201347. ACM Press, New York (2005)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-30482-1_22","volume-title":"Formal Methods and Software Engineering","author":"A. Armando","year":"2004","unstructured":"Armando, A., Castellini, C., Mantovani, J.: Software model checking using linear constraints. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 209\u2013223. Springer, Heidelberg (2004)"},{"key":"16_CR12","first-page":"79","volume-title":"SoftMC","author":"A. Armando","year":"2006","unstructured":"Armando, A., Benerecetti, M., Mantovani, J.: Model checking linear programs with arrays. In: SoftMC, pp. 79\u201394. Elsevier, Amsterdam (2006)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction-refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"16_CR15","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1145\/964001.964029","volume-title":"POPL","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330\u2013341. ACM Press, New York (2004)"},{"key":"16_CR16","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1109\/APAQS.2001.990006","volume-title":"APAQS: Asia-pacific conference on quality software","author":"J. Zhang","year":"2001","unstructured":"Zhang, J.: A path-based approach to the detection of infinite looping. In: APAQS: Asia-pacific conference on quality software, pp. 88\u201396. IEEE Computer Society, Los Alamitos (2001)"},{"key":"16_CR17","first-page":"106","volume-title":"ICS: International conference on Supercomputing","author":"R.A. Engelen van","year":"2004","unstructured":"van Engelen, R.A., Birch, J., Shou, Y., Walsh, B., Gallivan, K.A.: A unified framework for nonlinear dependence testing and symbolic analysis. In: ICS: International conference on Supercomputing, pp. 106\u2013115. ACM Press, New York (2004)"},{"key":"16_CR18","first-page":"343","volume-title":"POPL","author":"E.M. Clarke","year":"1992","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: POPL, pp. 343\u2013354. ACM Press, New York (1992)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-28644-8_1","volume-title":"CONCUR 2004 - Concurrency Theory","author":"T. Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Xie, Y.: Zing: Exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"16_CR22","volume-title":"The Science of Programming","author":"D. Gries","year":"1987","unstructured":"Gries, D.: The Science of Programming. Springer, Heidelberg (1987)"},{"key":"16_CR23","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems\u00a013, 451\u2013490 (1991)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR24","first-page":"105","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate Abstraction of ANSI\u2013C Programs using SAT. FMSD\u00a025, 105\u2013127 (2004)","journal-title":"FMSD"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"POPL","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244. ACM Press, New York (2004)"},{"key":"16_CR26","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: A backtrack search pseudo-Boolean solver. In: Theory and Appl. of Satisfiability Testing, pp. 346\u2013353 (2002)"},{"key":"16_CR27","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":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 268\u2013283. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T12:04:22Z","timestamp":1683547462000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/11817963_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}