{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T16:10:09Z","timestamp":1742659809680,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287169"},{"type":"electronic","value":"9783642287176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28717-6_14","type":"book-chapter","created":{"date-parts":[[2012,3,6]],"date-time":"2012-03-06T15:13:04Z","timestamp":1331046784000},"page":"153-167","source":"Crossref","is-referenced-by-count":14,"title":["Smart Testing of Functional Programs in Isabelle"],"prefix":"10.1007","author":[{"given":"Lukas","family":"Bulwahn","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"publisher","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\u00a047, 776\u2013822 (2000)","journal-title":"J. ACM"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-03359-9_11","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2009","unstructured":"Berghofer, S., Bulwahn, L., Haftmann, F.: Turning Inductive into Equational Specifications. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 131\u2013146. Springer, Heidelberg (2009)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Random Testing in Isabelle\/HOL. In: SEFM 2004, pp. 230\u2013239. IEEE Computer Society (2004)","DOI":"10.1109\/SEFM.2004.1347524"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"J.C. 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.\u00a06172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"14_CR5","unstructured":"Bulwahn, L.: Smart test data generators via logic programming. In: ICLP 2011 (Technical Communications). Leibniz Int. Proc. in Informatics, vol.\u00a011, pp. 139\u2013150. Schloss Dagstuhl, Leibniz-Zentrum f\u00fcr Informatik ( (2011)"},{"key":"14_CR6","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: Constraint Reasoning in FocalTest. In: ICSOFT 2010 (2010)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-78969-7_23","volume-title":"Functional and Logic Programming","author":"J. Christiansen","year":"2008","unstructured":"Christiansen, J., Fischer, S.: EasyCheck \u2014 Test Data for Free. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol.\u00a04989, pp. 322\u2013336. Springer, Heidelberg (2008)"},{"key":"14_CR8","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 SIGPLAN (2000)","DOI":"10.1145\/351240.351266"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Fischer, S., Kuchen, H.: Systematic generation of glass-box test cases for functional logic programs. In: PPDP 2007, pp. 63\u201374. ACM (2007)","DOI":"10.1145\/1273920.1273930"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code Generation via Higher-Order Rewrite Systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-540-74610-2_5","volume-title":"Logic Programming","author":"M. Hanus","year":"2007","unstructured":"Hanus, M.: Multi-paradigm Declarative Languages. In: Dahl, V., Niemel\u00e4, I. (eds.) ICLP 2007. LNCS, vol.\u00a04670, pp. 45\u201375. Springer, Heidelberg (2007)"},{"key":"14_CR12","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)"},{"key":"14_CR13","unstructured":"Lindblad, F.: Property directed generation of first-order test data. In: The Eigth Symposium on Trends in Functional Programming (2007)"},{"key":"14_CR14","unstructured":"Mellish, C.S.: The automatic generation of mode declarations for Prolog programs. Technical Report 163, Department of Artificial Intelligence (1981)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/3-540-54444-5_84","volume-title":"Programming Language Implementation and Logic Programming","author":"L. Naish","year":"1991","unstructured":"Naish, L.: Adding Equations to NU-Prolog. In: Ma\u0142uszy\u0144ski, J., Wirsing, M. (eds.) PLILP 1991. LNCS, vol.\u00a0528, pp. 15\u201326. Springer, Heidelberg (1991)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11921240_1","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"T. Nipkow","year":"2006","unstructured":"Nipkow, T.: Verifying a Hotel Key Card System. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 1\u201314. Springer, Heidelberg (2006)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Overton, D., Somogyi, Z., Stuckey, P.J.: Constraint-based mode analysis of mercury. In: PPDP 2002, pp. 109\u2013120. ACM (2002)","DOI":"10.1145\/571157.571169"},{"issue":"2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1023\/A:1022678217288","volume":"14","author":"C. Rouveirol","year":"1994","unstructured":"Rouveirol, C.: Flattening and Saturation: Two Representation Changes for Generalization. Mach. Learn.\u00a014(2), 219\u2013232 (1994)","journal-title":"Mach. Learn."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. In: Haskell 2008, pp. 37\u201348. ACM (2008)","DOI":"10.1145\/1411286.1411292"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/10720327_6","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J.G. Smaus","year":"2000","unstructured":"Smaus, J.G., Hill, P.M., King, A.: Mode Analysis Domains for Typed Logic Programs. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol.\u00a01817, pp. 82\u2013101. Springer, Heidelberg (2000)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Weber, T.: Bounded model generation for Isabelle\/HOL. In: PDPAR 2004. Electronic Notes in Theoretical Computer Science, vol.\u00a0125(3), pp. 103\u2013116. Elsevier (2005)","DOI":"10.1016\/j.entcs.2004.10.027"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 33\u201338. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28717-6_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T14:59:30Z","timestamp":1742655570000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28717-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287169","9783642287176"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28717-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}