{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:40:29Z","timestamp":1770280829236,"version":"3.49.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_15","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"447-491","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Predicate Abstraction for Program Verification"],"prefix":"10.1007","author":[{"given":"Ranjit","family":"Jhala","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"15_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1007\/978-3-642-31424-7_48","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp.\u00a0672\u2013678. Springer, Heidelberg (2012)"},{"key":"15_CR2","first-page":"203","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0203\u2013213. ACM, New York (2001)"},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T. Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transf. 5(1), 49\u201358 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR4","series-title":"LNCS","first-page":"113","volume-title":"Intl. Workshop on Model Checking Software (SPIN)","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.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol.\u00a01885, pp.\u00a0113\u2013130. Springer, Heidelberg (2000)"},{"key":"15_CR5","first-page":"1","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a01\u20133. ACM, New York (2002)"},{"key":"15_CR6","first-page":"221","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T.A. Beyene","year":"2014","unstructured":"Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: Jagannathan, S., Sewell, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0221\u2013234. ACM, New York (2014)"},{"key":"15_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"T.A. Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified Horn clauses. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a08044, pp.\u00a0869\u2013882. Springer, Heidelberg (2013)"},{"key":"15_CR8","first-page":"25","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"D. Beyer","year":"2009","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a025\u201332. IEEE, Piscataway (2009)"},{"key":"15_CR9","volume-title":"Handbook of Model Checking","author":"D. Beyer","year":"2018","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.A.: Combining model checking and data-flow analysis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"15_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06806, pp.\u00a0184\u2013190. Springer, Heidelberg (2011)"},{"key":"15_CR11","first-page":"189","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"D. Beyer","year":"2010","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0189\u2013197. IEEE, Piscataway (2010)"},{"key":"15_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-38856-9_8","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"N. Bj\u00f8rner","year":"2013","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a07935, pp.\u00a0105\u2013125. Springer, Heidelberg (2013)"},{"key":"15_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M. Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a08044, pp.\u00a0413\u2013429. Springer, Heidelberg (2013)"},{"key":"15_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-31424-7_13","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M. Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp.\u00a0105\u2013122. Springer, Heidelberg (2012)"},{"key":"15_CR15","first-page":"385","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"S. Chaki","year":"2003","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Clarke, L.A., Dillon, L., Tichy, W.F. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0385\u2013395. IEEE, Piscataway (2003)"},{"key":"15_CR16","series-title":"LNCS","first-page":"291","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"H.R. Chamarthi","year":"2011","unstructured":"Chamarthi, H.R., Dillinger, P.C., Manolios, P., Vroon, D.: The ACL2 Sedan theorem proving system. In: Abdulla, P.A., Leino, K.R.M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a06605, pp.\u00a0291\u2013295. Springer, Heidelberg (2011)"},{"key":"15_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","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.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0154\u2013169. Springer, Heidelberg (2000)"},{"key":"15_CR18","series-title":"LNCS","first-page":"570","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a03440, pp.\u00a0570\u2013574. Springer, Heidelberg (2005)"},{"key":"15_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-642-13754-9_4","volume-title":"Essays in Memory of Amir Pnueli","author":"E.M. Clarke","year":"2010","unstructured":"Clarke, E.M., Kurshan, R.P., Veith, H.: The localization reduction and counterexample-guided abstraction refinement. In: Manna, Z., Peled, D.A. (eds.) Essays in Memory of Amir Pnueli. LNCS, vol.\u00a06200, pp.\u00a061\u201371. Springer, Heidelberg (2010)"},{"key":"15_CR20","first-page":"415","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0415\u2013426. ACM, New York (2006)"},{"key":"15_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0415\u2013418. Springer, Heidelberg (2006)"},{"key":"15_CR22","series-title":"LNCS","first-page":"47","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"B. Cook","year":"2013","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a07795, pp.\u00a047\u201361. Springer, Heidelberg (2013)"},{"key":"15_CR23","first-page":"238","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0238\u2013252. ACM, New York (1977)"},{"key":"15_CR24","first-page":"245","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"2012","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: Field, J., Hicks, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0245\u2013258. ACM, New York (2012)"},{"issue":"3","key":"15_CR25","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"15_CR26","volume-title":"Handbook of Model Checking","author":"D. Dams","year":"2018","unstructured":"Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"15_CR27","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01633, pp.\u00a0160\u2013171. Springer, Heidelberg (1999)"},{"key":"15_CR28","series-title":"LNCS","first-page":"271","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"K. Dr\u00e4ger","year":"2010","unstructured":"Dr\u00e4ger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: a certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a06015, pp.\u00a0271\u2013274. Springer, Heidelberg (2010)"},{"key":"15_CR29","series-title":"LNCS","first-page":"500","volume-title":"Intl. Symp. on Formal Methods Europe (FME)","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) Intl. Symp. on Formal Methods Europe (FME). LNCS, vol.\u00a02021, pp.\u00a0500\u2013517. Springer, Heidelberg (2001)"},{"key":"15_CR30","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, pp.\u00a019\u201332. AMS, Providence (1967)"},{"key":"15_CR31","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01254, pp.\u00a072\u201383. Springer, Heidelberg (1997)"},{"key":"15_CR32","first-page":"405","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0405\u2013416. ACM, New York (2012)"},{"key":"15_CR33","first-page":"117","volume-title":"Intl. Symp. on Foundations of Software Engineering (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: Young, M., Devanbu, P.T. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0117\u2013127. ACM, New York (2006)"},{"key":"15_CR34","first-page":"331","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: Ball, T., Sagiv, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0331\u2013344. ACM, New York (2011)"},{"key":"15_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-22110-1_32","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06806, pp.\u00a0412\u2013417. Springer, Heidelberg (2011)"},{"key":"15_CR36","first-page":"471","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"M. Heizmann","year":"2010","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0471\u2013482. ACM, New York (2010)"},{"key":"15_CR37","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-15769-1_4","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"M. Heizmann","year":"2010","unstructured":"Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants. In: Cousot, R., Martel, M. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a06337, pp.\u00a022\u201350. Springer, Heidelberg (2010)"},{"key":"15_CR38","first-page":"232","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0232\u2013244. ACM, New York (2004)"},{"key":"15_CR39","first-page":"58","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Launchbury, J., Mitchell, J.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a058\u201370. ACM, New York (2002)"},{"issue":"10","key":"15_CR40","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"15_CR41","first-page":"297","volume-title":"International Conference on Computer Design (ICCD)","author":"F. Ivancic","year":"2005","unstructured":"Ivancic, F., Shlyakhter, I., Gupta, A., Ganai, M.K.: Model checking C programs using F-SOFT. In: International Conference on Computer Design (ICCD), pp.\u00a0297\u2013308. IEEE, Piscataway (2005)"},{"issue":"4","key":"15_CR42","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R. Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009)","journal-title":"ACM Comput. Surv."},{"key":"15_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04590, pp.\u00a0193\u2013206. Springer, Heidelberg (2007)"},{"key":"15_CR44","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Kroening","year":"2010","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06174, pp.\u00a089\u2013103. Springer, Heidelberg (2010)"},{"key":"15_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-642-22110-1_45","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Kroening","year":"2011","unstructured":"Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06806, pp.\u00a0573\u2013578. Springer, Heidelberg (2011)"},{"key":"15_CR46","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-27813-9_11","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03114, pp.\u00a0135\u2013147. Springer, Heidelberg (2004)"},{"key":"15_CR47","first-page":"81","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"C.S. Lee","year":"2001","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Hankin, C., Schmidt, D. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a081\u201392. ACM, New York (2001)"},{"key":"15_CR48","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-31424-7_12","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"W. Lee","year":"2012","unstructured":"Lee, W., Wang, B., Yi, K.: Termination analysis with algorithmic learning. In: Madhusudan, P., Seshia, S.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp.\u00a088\u2013104. Springer, Heidelberg (2012)"},{"key":"15_CR49","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0123\u2013136. Springer, Heidelberg (2006)"},{"key":"15_CR50","series-title":"LNCS","first-page":"178","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A.V. Nori","year":"2009","unstructured":"Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The Yogi project: software property checking via static analysis and testing. In: Kowalewski, S., Philippou, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a05505, pp.\u00a0178\u2013181. Springer, Heidelberg (2009)"},{"key":"15_CR51","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","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.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a02937, pp.\u00a0239\u2013251. Springer, Heidelberg (2004)"},{"key":"15_CR52","first-page":"32","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Symp. on Logic in Computer Science (LICS), pp.\u00a032\u201341. IEEE, Piscataway (2004)"},{"key":"15_CR53","first-page":"132","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Palsberg, J., Abadi, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0132\u2013144. ACM, New York (2005)"},{"key":"15_CR54","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages (PADL)","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.A.: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) Practical Aspects of Declarative Languages (PADL). LNCS, vol.\u00a04354, pp.\u00a0245\u2013259. Springer, Heidelberg (2007)"},{"key":"15_CR55","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11547662_19","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a03672, pp.\u00a0268\u2013283. Springer, Heidelberg (2005)"},{"key":"15_CR56","first-page":"249","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"A. Podelski","year":"2010","unstructured":"Podelski, A., Wies, T.: Counterexample-guided focus. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0249\u2013260. ACM, New York (2010)"},{"key":"15_CR57","first-page":"159","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"P.M. Rondon","year":"2008","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Gupta, R., Amarasinghe, S.P. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0159\u2013169. ACM, New York (2008)"},{"issue":"3","key":"15_CR58","doi-asserted-by":"publisher","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. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T01:44:36Z","timestamp":1571363076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_15","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}