{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T11:33:45Z","timestamp":1778672025778,"version":"3.51.4"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,6,1]],"date-time":"2016-06-01T00:00:00Z","timestamp":1464739200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,6,1]],"date-time":"2016-06-01T00:00:00Z","timestamp":1464739200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DMS1068829"],"award-info":[{"award-number":["DMS1068829"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS0926181"],"award-info":[{"award-number":["CNS0926181"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS0931985"],"award-info":[{"award-number":["CNS0931985"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Gigascale Systems Research Center","award":["1041377"],"award-info":[{"award-number":["1041377"]}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["2005TJ1366"],"award-info":[{"award-number":["2005TJ1366"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N000141010188"],"award-info":[{"award-number":["N000141010188"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CMU-Portugal Program"},{"DOI":"10.13039\/100000005","name":"U.S. Department of Defense","doi-asserted-by":"publisher","award":["FA8721-05-C-0003"],"award-info":[{"award-number":["FA8721-05-C-0003"]}],"id":[{"id":"10.13039\/100000005","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s10703-016-0249-4","type":"journal-article","created":{"date-parts":[[2016,8,25]],"date-time":"2016-08-25T13:13:00Z","timestamp":1472130780000},"page":"175-205","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":104,"title":["SMT-based model checking for recursive programs"],"prefix":"10.1007","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0927-2075","authenticated-orcid":false,"given":"Anvesh","family":"Komuravelli","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Sagar","family":"Chaki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,25]]},"reference":[{"key":"249_CR1","unstructured":"Ball T, Rajamani SK (2000) Bebop: a symbolic model checker for Boolean programs. In: SPIN, pp 113\u2013130"},{"issue":"5","key":"249_CR2","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 SK (2001) Automatic predicate abstraction of C programs. SIGPLAN Not 36(5):203\u2013213","journal-title":"SIGPLAN Not"},{"key":"249_CR3","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"249_CR4","unstructured":"Barnett M, Chang B-YE, DeLine R, Jacobs B, Leino KRM (2005) Boogie: a modular reusable verifier for object-oriented programs. In: FMCO, pp 364\u2013387"},{"key":"249_CR5","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M (2012) From under-approximations to over-approximations and back. In: TACAS","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"249_CR6","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI, pp 405\u2013416","DOI":"10.1145\/2254064.2254112"},{"issue":"1","key":"249_CR7","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"EM Clarke","year":"1979","unstructured":"Clarke EM (1979) Programming language constructs for which it is impossible to obtain good Hoare axiom systems. JACM 26(1):129\u2013147","journal-title":"JACM"},{"key":"249_CR8","doi-asserted-by":"crossref","unstructured":"Reps TW, Horwitz S, Sagiv S (1995) Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp 49\u201361","DOI":"10.1145\/199448.199462"},{"issue":"4","key":"249_CR9","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BF02248730","volume":"21","author":"EM Clarke","year":"1979","unstructured":"Clarke EM (1979) Program invariants as fixed points. Computing 21(4):273\u2013294","journal-title":"Computing"},{"key":"249_CR10","unstructured":"Sharir M, Pnueli A (1981) Program flow analysis: theory and applications. In: Two approaches to interprocedural data flow analysis. Prentice-Hall, pp 189\u2013233"},{"issue":"4","key":"249_CR11","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 (2005) Analysis of recursive state machines. TOPLAS 27(4):786\u2013818","journal-title":"TOPLAS"},{"key":"249_CR12","doi-asserted-by":"crossref","unstructured":"Esparza J, Hansel D, Rossmanith P, Schwoon S (2000) Efficient algorithms for model checking pushdown systems. In: CAV, pp 232\u2013247","DOI":"10.1007\/10722167_20"},{"key":"249_CR13","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: CAV","DOI":"10.1007\/10722167_15"},{"key":"249_CR14","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI, pp 39\u201355","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"249_CR15","doi-asserted-by":"crossref","unstructured":"Hoder K, Bj\u00f8rner N (2012) Generalized property directed reachability. In: SAT","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"249_CR16","first-page":"641","volume-title":"TACAS, lecture notes in computer science","author":"M Heizmann","year":"2013","unstructured":"Heizmann M, Christ J, Dietsch D, Ermis E, Hoenicke J, Lindenmann M, Nutz A, Schilling C, Podelski A (2013) Ultimate automizer with SMTInterpol\u2014(competition contribution). In: Piterman N, Smolka SA (eds) TACAS, lecture notes in computer science, vol 7795. Springer, Heidelberg, pp 641\u2013643"},{"issue":"1","key":"249_CR17","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 (2010) Nested interpolants. SIGPLAN Not 45(1):471\u2013482 1","journal-title":"SIGPLAN Not"},{"key":"249_CR18","unstructured":"McMillan KL, Rybalchenko A (2013) Solving constrained horn clauses using interpolation. Technical Report MSR-TR-2013-6, Microsoft Research"},{"key":"249_CR19","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 EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:117\u2013148","journal-title":"Adv Comput"},{"issue":"3","key":"249_CR20","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Symb Logic 22(3):269\u2013285","journal-title":"Symb Logic"},{"issue":"4","key":"249_CR21","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 (2005) Analysis of recursive state machines. ACM Trans Program Lang Syst 27(4):786\u2013818","journal-title":"ACM Trans Program Lang Syst"},{"key":"249_CR22","doi-asserted-by":"crossref","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: VMCAI","DOI":"10.1007\/978-3-642-18275-4_7"},{"issue":"5","key":"249_CR23","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos R, Weispfenning V (1993) Applying linear quantifier elimination. Computing 36(5):450\u2013462","journal-title":"Computing"},{"issue":"91\u2014-100","key":"249_CR24","first-page":"300","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper DC (1972) Theorem proving in arithmetic without multiplication. Mach Intel 7(91\u2014-100):300","journal-title":"Mach Intel"},{"issue":"6","key":"249_CR25","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 (2006) Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"key":"249_CR26","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"249_CR27","doi-asserted-by":"crossref","unstructured":"Ganai MK, Gupta A, Ashar P (2004) Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: ICCAD, pp 510\u2013517","DOI":"10.1109\/ICCAD.2004.1382631"},{"issue":"2","key":"249_CR28","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T Nipkow","year":"2010","unstructured":"Nipkow T (2010) Linear quantifier elimination. J Autom Reason 45(2):189\u2013212","journal-title":"J Autom Reason"},{"key":"249_CR29","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gurfinkel A, Li Y, Chaki S, Chechik M (2013) UFO: verification with interpolants and abstract interpretation\u2014(competition contribution). In: TACAS","DOI":"10.1007\/978-3-642-36742-7_52"},{"key":"249_CR30","unstructured":"Software Verification Competition. TACAS, 2014. \n                    http:\/\/sv-comp.sosy-lab.org"},{"key":"249_CR31","unstructured":"Komuravelli A, Gurfinkel A, Chaki S, Clarke EM (2013) Automated abstraction in SMT-based unbounded software model checking. In: CAV, pp 846\u2013862"},{"key":"249_CR32","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of the POPL, pp 58\u201370","DOI":"10.1145\/503272.503279"},{"issue":"6","key":"249_CR33","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S Chaki","year":"2004","unstructured":"Chaki S, Clarke EM, Groce A, Jha S, Veith H (2004) Modular verification of software components in C. IEEE Trans Softw Eng 30(6):388\u2013402","journal-title":"IEEE Trans Softw Eng"},{"key":"249_CR34","doi-asserted-by":"crossref","unstructured":"Godefroid P, Nori AV, Rajamani SK, Tetali S (2010) Compositional may-must program analysis: unleashing the power of alternation. In: POPL, pp 43\u201356","DOI":"10.1145\/1706299.1706307"},{"key":"249_CR35","first-page":"427","volume-title":"CAV, lecture notes in computer science","author":"A Lal","year":"2012","unstructured":"Lal A, Qadeer S, Lahiri SK (2012) A solver for reachability modulo theories. In: Madhusudan P, Seshia SA (eds) CAV, lecture notes in computer science, vol 7358. Springer, Heidelberg, pp 427\u2013443"},{"key":"249_CR36","doi-asserted-by":"crossref","unstructured":"Gupta A, Ganai MK, Yang Z, Ashar P (2003) Iterative abstraction using SAT-based BMC with proof analysis. In: ICCAD, pp 416\u2013423","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"249_CR37","doi-asserted-by":"crossref","unstructured":"McMillan KL, Amla N (2003) Automatic abstraction without counterexamples. In: TACAS","DOI":"10.1007\/3-540-36577-X_2"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0249-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0249-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0249-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0249-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:43:00Z","timestamp":1589730180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0249-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["249"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0249-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6]]},"assertion":[{"value":"25 August 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}