{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:54:45Z","timestamp":1768002885755,"version":"3.49.0"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,3,29]],"date-time":"2016-03-29T00:00:00Z","timestamp":1459209600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,12]]},"DOI":"10.1007\/s10817-016-9368-2","type":"journal-article","created":{"date-parts":[[2016,3,29]],"date-time":"2016-03-29T05:06:52Z","timestamp":1459228012000},"page":"281-318","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Reasoning About Algebraic Data Types with Abstractions"],"prefix":"10.1007","volume":"57","author":[{"given":"Tuan-Hung","family":"Pham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,29]]},"reference":[{"key":"9368_CR1","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"8","key":"9368_CR2","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.entcs.2006.11.037","volume":"174","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. Electron. Notes Theor. Comput. Sci. 174(8), 23\u201337 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9368_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: SMT (2010)"},{"key":"9368_CR4","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the leon verification system: verification by translation to recursive functions. In: SCALA, pp. 1:1\u20131:10 (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"9368_CR5","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: TACAS, pp. 150\u2013153 (2010)","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"9368_CR6","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9368_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511801655","volume-title":"Analytic Combinatorics","author":"P Flajolet","year":"2009","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics. Cambridge University Press, Cambridge (2009)"},{"key":"9368_CR8","doi-asserted-by":"crossref","unstructured":"Hardin, D., Slind, K., Whalen, M., Pham, T.H.: The guardol language and verification system. In: TACAS, pp. 18\u201332 (2012)","DOI":"10.1007\/978-3-642-28756-5_3"},{"key":"9368_CR9","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Kuncak, V.: Towards Complete Reasoning about Axiomatic Specifications. In: VMCAI, pp. 278\u2013293 (2011)","DOI":"10.1007\/978-3-642-18275-4_20"},{"key":"9368_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: ACL2 Case Studies. Springer, Heidelberg (2000)"},{"key":"9368_CR11","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI, pp. 222\u2013233 (2011)","DOI":"10.1145\/1993498.1993525"},{"key":"9368_CR12","volume-title":"Catalan Numbers with Applications","author":"T Koshy","year":"2009","unstructured":"Koshy, T.: Catalan Numbers with Applications. Oxford University Press, Oxford (2009)"},{"key":"9368_CR13","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR, pp. 348\u2013370 (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"9368_CR14","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL, pp. 611\u2013622 (2011)","DOI":"10.1145\/1926385.1926455"},{"key":"9368_CR15","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Qiu, X., Stefanescu, A.: Recursive proofs for inductive tree data-structures. In: POPL, pp. 123\u2013136 (2012)","DOI":"10.1145\/2103656.2103673"},{"key":"9368_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)"},{"issue":"3","key":"9368_CR17","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning About Recursively Defined Data Structures. J. ACM 27(3), 403\u2013411 (1980)","journal-title":"J. ACM"},{"key":"9368_CR18","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: CADE, pp. 748\u2013752 (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9368_CR19","unstructured":"Pham, T.H.: Verification of recursive data types using abstractions. Ph.D. thesis, University of Minnesota (2014)"},{"key":"9368_CR20","doi-asserted-by":"crossref","unstructured":"Pham, T.H., Whalen, M.: An improved unrolling-based decision procedure for algebraic data types. In: VSTTE (2013)","DOI":"10.1007\/978-3-642-54108-7_7"},{"key":"9368_CR21","unstructured":"Pham, T.H., Whalen, M.W.: Parameterized abstractions for reasoning about algebraic data types. In: CFV (2013). Available at http:\/\/www-users.cs.umn.edu\/~hung\/papers\/cfv13"},{"key":"9368_CR22","doi-asserted-by":"crossref","unstructured":"Pham, T.H., Whalen, M.W.: RADA: A tool for reasoning about algebraic data types with abstractions. In: ESEC\/SIGSOFT FSE, pp. 611\u2013614 (2013)","DOI":"10.1145\/2491411.2494597"},{"key":"9368_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Kuncak, V., Induction for SMT Solvers. In: VMCAI, (2015)","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"9368_CR24","doi-asserted-by":"crossref","unstructured":"Sato, R., Unno, H., Kobayashi, N.: Towards a Scalable Software Model Checker for Higher-Order Programs. In: PEPM, pp. 53\u201362 (2013)","DOI":"10.1145\/2426890.2426900"},{"key":"9368_CR25","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: CADE, pp. 67\u201383 (2009)","DOI":"10.1007\/978-3-642-02959-2_5"},{"key":"9368_CR26","volume-title":"Enumerative Combinatorics","author":"RP Stanley","year":"2001","unstructured":"Stanley, R.P.: Enumerative Combinatorics, vol. 2. Cambridge University Press, Cambridge (2001)"},{"key":"9368_CR27","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL, pp. 199\u2013210 (2010)","DOI":"10.1145\/1706299.1706325"},{"key":"9368_CR28","doi-asserted-by":"crossref","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: SAS (2011)","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"9368_CR29","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI, pp. 349\u2013361 (2008)","DOI":"10.1145\/1375581.1375624"},{"key":"9368_CR30","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: An integrated proof language for imperative programs. In: PLDI, pp. 338\u2013351 (2009)","DOI":"10.1145\/1542476.1542514"},{"key":"9368_CR31","doi-asserted-by":"crossref","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. In: Information and Computation, pp. 152\u2013167 (2004)","DOI":"10.1007\/978-3-540-25984-8_9"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9368-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9368-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9368-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9368-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,6]],"date-time":"2019-09-06T01:50:16Z","timestamp":1567734616000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9368-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,29]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,12]]}},"alternative-id":["9368"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9368-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,29]]}}}