{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:02Z","timestamp":1776333542118,"version":"3.51.2"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319088662","type":"print"},{"value":"9783319088679","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_2","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:37:30Z","timestamp":1403955450000},"page":"17-34","source":"Crossref","is-referenced-by-count":119,"title":["SMT-Based Model Checking for Recursive Programs"],"prefix":"10.1007","author":[{"given":"Anvesh","family":"Komuravelli","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Sagar","family":"Chaki","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-28756-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From Under-Approximations to Over-Approximations and Back. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 157\u2013172. Springer, Heidelberg (2012)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-27940-9_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 39\u201355. Springer, Heidelberg (2012)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/978-3-642-36742-7_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., Gurfinkel, A., Li, Y., Chaki, S., Chechik, M.: UFO: Verification with Interpolants and Abstract Interpretation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 637\u2013640. Springer, Heidelberg (2013)"},{"issue":"4","key":"2_CR4","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R. Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of Recursive State Machines. TOPLAS\u00a027(4), 786\u2013818 (2005)","journal-title":"TOPLAS"},{"issue":"5","key":"2_CR5","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. SIGPLAN Not.\u00a036(5), 203\u2013213 (2001)","journal-title":"SIGPLAN Not."},{"key":"2_CR6","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":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers\u00a058, 117\u2013148 (2003)","journal-title":"Advances in Computers"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"issue":"6","key":"2_CR10","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. Software Eng.\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Trans. Software Eng."},{"issue":"4","key":"2_CR11","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BF02248730","volume":"21","author":"E.M. Clarke","year":"1979","unstructured":"Clarke, E.M.: Program Invariants as Fixed Points. Computing\u00a021(4), 273\u2013294 (1979)","journal-title":"Computing"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E.M. Clarke","year":"1979","unstructured":"Clarke, E.M.: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems. JACM\u00a026(1), 129\u2013147 (1979)","journal-title":"JACM"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: CAV (2000)","DOI":"10.1007\/10722167_15"},{"key":"2_CR14","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., Kroning, 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":"2_CR15","unstructured":"Cooper, D.C.: Theorem Proving in Arithmetic without Multiplication. In: Machine Intelligence, pp. 91\u2013100 (1972)"},{"issue":"3","key":"2_CR16","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"Symbolic Logic"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR19","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":"2_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional May-Must Program Analysis: Unleashing the Power of Alternation. In: POPL, pp. 43\u201356 (2010)","DOI":"10.1145\/1707801.1706307"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing Software Verifiers from Proof Rules. In: PLDI, pp. 405\u2013416 (2012)","DOI":"10.1145\/2345156.2254112"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Gupta, A., Ganai, M.K., Yang, Z., Ashar, P.: Iterative Abstraction using SAT-based BMC with Proof Analysis. In: ICCAD, pp. 416\u2013423 (2003)","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-88387-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"A. Gurfinkel","year":"2008","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Model checking recursive programs with exact predicate abstraction. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 95\u2013110. Springer, Heidelberg (2008)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-642-36742-7_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Heizmann","year":"2013","unstructured":"Heizmann, M., Christ, J., Dietsch, D., Ermis, E., Hoenicke, J., Lindenmann, M., Nutz, A., Schilling, C., Podelski, A.: Ultimate Automizer with SMTInterpol. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 641\u2013643. Springer, Heidelberg (2013)"},{"issue":"1","key":"2_CR25","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/1707801.1706353","volume":"45","author":"M. Heizmann","year":"2010","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Nested Interpolants. SIGPLAN Not.\u00a045(1), 471\u2013482 (2010)","journal-title":"SIGPLAN Not."},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K. Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized Property Directed Reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based Model Checking for Recursive Programs. CoRR, abs\/1405.4028 (2014)","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/978-3-642-39799-8_59","volume-title":"Computer Aided Verification","author":"A. Komuravelli","year":"2013","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 846\u2013862. Springer, Heidelberg (2013)"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 427\u2013443. Springer, Heidelberg (2012)"},{"issue":"5","key":"2_CR31","first-page":"450","volume":"36","author":"R. Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying Linear Quantifier Elimination. Computing\u00a036(5), 450\u2013462 (1993)","journal-title":"Computing"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"key":"2_CR33","unstructured":"McMillan, K.L., Rybalchenko, A.: Solving Constrained Horn Clauses using Interpolation. Technical Report MSR-TR-2013-6, Microsoft Research (2013)"},{"issue":"6","key":"2_CR34","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"2","key":"2_CR35","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T. Nipkow","year":"2010","unstructured":"Nipkow, T.: Linear Quantifier Elimination. J. Autom. Reason.\u00a045(2), 189\u2013212 (2010)","journal-title":"J. Autom. Reason."},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Horwitz, S., Sagiv, S.: Precise Interprocedural Dataflow Analysis via Graph Reachability. In: POPL, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"2_CR37","unstructured":"Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. In: Program Flow Analysis: Theory and Applications, pp. 189\u2013233. Prentice-Hall (1981)"},{"key":"2_CR38","unstructured":"Software Verification Competition. TACAS (2014), http:\/\/sv-comp.sosy-lab.org"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T14:01:50Z","timestamp":1746280910000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}