{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:17Z","timestamp":1725903377266},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_8","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:34:07Z","timestamp":1499679247000},"page":"114-129","source":"Crossref","is-referenced-by-count":2,"title":["Satisfiability Modulo Bounded Checking"],"prefix":"10.1007","author":[{"given":"Simon","family":"Cruanes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1145\/347476.347484","volume":"47","author":"S Antoy","year":"2000","unstructured":"Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM (JACM) 47, 776\u2013822 (2000)","journal-title":"J. ACM (JACM)"},{"key":"8_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard Version 2.6 (2016). \nhttp:\/\/www.SMT-LIB.org"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006). doi:\n10.1007\/11916277_35"},{"issue":"8","key":"8_CR4","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."},{"issue":"4","key":"8_CR5","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/1988042.1988046","volume":"46","author":"K Claessen","year":"2011","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM Sigplan Not. 46(4), 53\u201364 (2011)","journal-title":"ACM Sigplan Not."},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-20615-8_23","volume-title":"Intelligent Computer Mathematics","author":"K Claessen","year":"2015","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 333\u2013337. Springer, Cham (2015). doi:\n10.1007\/978-3-319-20615-8_23"},{"key":"8_CR7","unstructured":"Claessen, K., Ros\u00e9n, D.: SAT-based bounded model checking for functional programs (2016) (unpublished). \nhttps:\/\/github.com\/danr\/hbmc"},{"key":"8_CR8","unstructured":"The Coq Development Team. The Coq Proof Assistant. \nhttp:\/\/coq.inria.fr\/"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Cruanes, S., Blanchette, J.C.: Extending Nunchaku to dependent type theory. In: Blanchette, J.C., Kaliszyk, C. (eds.) Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016. EPTCS, vol. 210, Coimbra, Portugal, pp. 3\u201312, 1 July 2016","DOI":"10.4204\/EPTCS.210.3"},{"issue":"12","key":"8_CR10","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1145\/2430532.2364515","volume":"47","author":"J Dureg\u00e5rd","year":"2013","unstructured":"Dureg\u00e5rd, J., Jansson, P., Wang, M.: Feat: functional enumeration of algebraic types. ACM SIGPLAN Not. 47(12), 61\u201372 (2013)","journal-title":"ACM SIGPLAN Not."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Hanus, M.: A unified computation model for functional and logic programming. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (1997)","DOI":"10.1145\/263699.263710"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Moore, S.J.: ACL2: an industrial strength version of Nqthm. In: Computer Assurance, COMPASS 1996, pp. 23\u201334. IEEE (1996)","DOI":"10.1109\/CMPASS.1996.507872"},{"issue":"1","key":"8_CR13","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"RE Korf","year":"1985","unstructured":"Korf, R.E.: Depth-first iterative-deepening: an optimal admissible tree search. Artif. Intell. 27(1), 97\u2013109 (1985)","journal-title":"Artif. Intell."},{"key":"8_CR14","unstructured":"Lindblad, F.: Property directed generation of first-order test data. In: Trends in Functional Programming, pp. 105\u2013123. Citeseer (2007)"},{"key":"8_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover, vol. 828. Springer, Heidelberg (1994)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 197\u2013213. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21401-6_13"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-319-40229-1_10","volume-title":"Automated Reasoning","author":"A Reynolds","year":"2016","unstructured":"Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 133\u2013151. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40229-1_10"},{"key":"8_CR18","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/1543134.1411292","volume":"44","author":"C Runciman","year":"2008","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. ACM SIGPLAN Not. 44, 37\u201348 (2008). ACM","journal-title":"ACM SIGPLAN Not."},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Static Analysis","author":"P Suter","year":"2011","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 298\u2013315. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-23702-7_23"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T09:36:08Z","timestamp":1499679368000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}