{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:57:23Z","timestamp":1725857843166},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_10","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T12:54:04Z","timestamp":1465649644000},"page":"133-151","source":"Crossref","is-referenced-by-count":12,"title":["Model Finding for Recursive Functions in SMT"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Cruanes","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: Morrisett, G., Uustalu, T. (eds.) ICFP 2013, pp. 197\u2013208. ACM (2013)","DOI":"10.1145\/2500365.2500597"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"10_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard\u2013Version 2.5. Technical report, The University of Iowa (2015). http:\/\/smt-lib.org\/"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-642-45221-5_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Bax, J.: Proving infinite satisfiability. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 86\u201395. Springer, Heidelberg (2013)"},{"issue":"1","key":"10_CR5","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1016\/j.jal.2007.07.005","volume":"7","author":"P Baumgartner","year":"2009","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7(1), 58\u201374 (2009)","journal-title":"J. Appl. Log."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system\u2013Verification by translation to recursive functions. In: Scala 2013. ACM (2013)","DOI":"10.1145\/2489837.2489838"},{"issue":"1","key":"10_CR7","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/s11219-011-9148-5","volume":"21","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C.: Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions. Softw. Qual. J. 21(1), 101\u2013126 (2013)","journal-title":"Softw. Qual. J."},{"issue":"1","key":"10_CR8","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reasoning 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"10_CR9","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/s10817-011-9234-1","volume":"47","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. J. Autom. Reasoning 47(4), 369\u2013398 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: Reppy, J. (ed.) ICFP 2015. ACM (2015)","DOI":"10.1145\/2784731.2784732"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: ICFP 2000, pp. 268\u2013279. ACM (2000)","DOI":"10.1145\/351240.351266"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/978-3-642-22438-6_17","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Claessen","year":"2011","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 207\u2013221. Springer, Heidelberg (2011)"},{"key":"10_CR14","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: MODEL (2003)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Efficient E-Matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"10_CR16","unstructured":"de Moura, L., Bj\u00f8rner, N.: Relevancy propagation. Technical report, Microsoft Research, October 2007"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"4","key":"10_CR18","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/s10817-010-9166-1","volume":"45","author":"A Dunets","year":"2010","unstructured":"Dunets, A., Schellhorn, G., Reif, W.: Automated flaw detection in algebraic specifications. J. Autom. Reasoning 45(4), 359\u2013395 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"issue":"1","key":"10_CR20","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95\u2013146 (1992)","journal-title":"J. ACM"},{"key":"10_CR21","unstructured":"Jackson, D.: Nitpick: a checkable specification language. In: FMSP 1996, pp. 60\u201369 (1996)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-642-14052-5_21","volume-title":"Interactive Theorem Proving","author":"M Johansson","year":"2010","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Case-analysis for rippling and inductive proof. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 291\u2013306. Springer, Heidelberg (2010)"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/978-3-642-40885-4_15","volume-title":"Frontiers of Combining Systems","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 214\u2013228. Springer, Heidelberg (2013)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Krauss, A.: Automating recursive definitions and termination proofs in higher-order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)","DOI":"10.1007\/s10817-009-9157-2"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Jackson, D.: Relational analysis of algebraic datatypes. In: Wermelinger, M., Gall, H. (eds.) ESEC\/FSE 2005. ACM (2005)","DOI":"10.1145\/1095430.1081740"},{"key":"10_CR26","unstructured":"Lindblad, F.: Property directed generation of first-order test data. In: Moraz\u00e1n, M. (ed.) TFP 2007, pp. 105\u2013123. Intellect (2008)"},{"key":"10_CR27","unstructured":"McCune, W.: Prover9 and Mace4. http:\/\/www.cs.unm.edu\/mccune\/prover9\/"},{"key":"10_CR28","unstructured":"McCune, W.: A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problems. Technical report, Argonne National Laboratory (1994)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-319-21401-6_13","volume-title":"Automated Deduction - CADE-25","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Felty, A., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 197\u2013213. Springer, Heidelberg (2015)"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Blanchette, J.C., Tinelli, C.: Model finding for recursive functions in SMT. In: Ganesh, V., Jovanovi\u0107, D. (eds.) SMT 2015 (2015)","DOI":"10.1007\/978-3-319-40229-1_10"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD 2014, pp. 195\u2013202. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013)"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/978-3-642-38574-2_26","volume-title":"Automated Deduction \u2013 CADE-24","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 377\u2013391. Springer, Heidelberg (2013)"},{"key":"10_CR34","unstructured":"Reynolds, A.J.: Finite model finding in satisfiability modulo theories. Ph.D. thesis, The University of Iowa (2013)"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. In: Gill, A. (ed.) Haskell 2008, pp. 37\u201348. ACM (2008)","DOI":"10.1145\/1411286.1411292"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1007\/3-540-58156-1_63","volume-title":"Automated Deduction - CADE-12","author":"JK Slaney","year":"1994","unstructured":"Slaney, J.K.: FINDER: finite domain enumerator system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 798\u2013801. Springer, Heidelberg (1994)"},{"key":"10_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"10_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-60675-0_35","volume-title":"Functional Programming Languages in Education","author":"DA Turner","year":"1995","unstructured":"Turner, D.A.: Elementary strong functional programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, pp. 1\u201313. Springer, Heidelberg (1995)"},{"key":"10_CR39","unstructured":"Weber, T.: SAT-based finite model generation for higher-order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2008)"},{"key":"10_CR40","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Mellish, C.S. (ed.) IJCAI 1995, vol. 1, pp. 298\u2013303. Morgan Kaufmann (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,1]],"date-time":"2022-07-01T15:41:30Z","timestamp":1656690090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}