{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:39Z","timestamp":1774837839359,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642353079","type":"print"},{"value":"9783642353086","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_10","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"92-108","source":"Crossref","is-referenced-by-count":45,"title":["The New Quickcheck for Isabelle"],"prefix":"10.1007","author":[{"given":"Lukas","family":"Bulwahn","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Cuellar, J., Liu, Z. (eds.) SEFM 2004, pp. 230\u2013239. IEEE C.S. (2004)","DOI":"10.1109\/SEFM.2004.1347524"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol.\u00a06989, pp. 12\u201327. Springer, Heidelberg (2011)"},{"key":"10_CR3","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":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-28717-6_14","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Bulwahn","year":"2012","unstructured":"Bulwahn, L.: Smart Testing of Functional Programs in Isabelle. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 153\u2013167. Springer, Heidelberg (2012)"},{"key":"10_CR5","unstructured":"Chamarthi, H.R., Dillinger, P., Kaufmann, M., Manolios, P.: Integrating testing and interactive theorem proving (2011), http:\/\/arxiv.org\/pdf\/1105.4394"},{"key":"10_CR6","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":"10_CR7","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\/357766.351266"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/10930755_12","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Dybjer","year":"2003","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining Testing and Proving in Dependent Type Theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 188\u2013203. Springer, Heidelberg (2003)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Eastlund, C.: Doublecheck your theorems. In: 8th Int. Workshop on the ACL2 Theorem Prover and its Applications (2009)","DOI":"10.1145\/1637837.1637844"},{"key":"10_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":"10_CR11","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_CR12","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":"10_CR13","series-title":"Lecture Notes in Computer Science","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., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"10_CR14","unstructured":"Owre, S.: Random testing in PVS. In: AFM 2006 (2006)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values. In: Haskell Symp. 2008, pp. 37\u201348 (2008)","DOI":"10.1145\/1411286.1411292"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-15975-4_33","volume-title":"Functional Programming Languages and Computer Architecture","author":"P. Wadler","year":"1985","unstructured":"Wadler, P.: How to Replace Failure by a List of Successes. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol.\u00a0201, pp. 113\u2013128. Springer, Heidelberg (1985)"},{"key":"10_CR17","unstructured":"Weber, T.: SAT-based Finite Model Generation for Higher-Order Logic. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany (2008)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type Classes and Overloading in Higher-order Logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T12:19:30Z","timestamp":1745151570000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_10"}},"subtitle":["Random, Exhaustive and Symbolic Testing under One Roof"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}