{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:41Z","timestamp":1780994801696,"version":"3.54.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319221014","type":"print"},{"value":"9783319221021","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_22","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"325-343","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":43,"title":["Foundational Property-Based Testing"],"prefix":"10.1007","author":[{"given":"Zoe","family":"Paraskevopoulou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maxime","family":"D\u00e9n\u00e8s","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonidas","family":"Lampropoulos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"22_CR1","unstructured":"Appel, A.W.: Efficient verified red-black trees, Manuscript (2011)"},{"key":"22_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. 5674, pp. 131\u2013146. Springer, Heidelberg (2009)"},{"issue":"1","key":"22_CR3","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1002\/stvr.1544","volume":"25","author":"AD Brucker","year":"2015","unstructured":"Brucker, A.D., Br\u00fcgger, L., Wolff, B.: Formal firewall conformance testing: an application of test and proof techniques. Softw. Test. Verification Reliab. 25(1), 34\u201371 (2015)","journal-title":"Softw. Test. Verification Reliab."},{"issue":"5","key":"22_CR4","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/s00165-012-0222-y","volume":"25","author":"AD Brucker","year":"2013","unstructured":"Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Aspects Comput. 25(5), 683\u2013721 (2013)","journal-title":"Formal Aspects Comput."},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-35308-6_10","volume-title":"Certified Programs and Proofs","author":"L Bulwahn","year":"2012","unstructured":"Bulwahn, L.: The new quickcheck for Isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92\u2013108. Springer, Heidelberg (2012)"},{"key":"22_CR6","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. 7180, pp. 153\u2013167. Springer, Heidelberg (2012)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-30473-6_5","volume-title":"Tests and Proofs","author":"M Carlier","year":"2012","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: A first step in the design of a formally verified constraint-based testing tool: focaltest. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 35\u201350. Springer, Heidelberg (2012)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Chamarthi, H.R., Dillinger, P.C., Kaufmann, M., Manolios, P.: Integrating testing and interactive theorem proving. In: 10th International Workshop on the ACL2 Theorem Prover and its Applications. EPTCS, vol. 70, pp. 4\u201319 (2011)","DOI":"10.4204\/EPTCS.70.1"},{"key":"22_CR9","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. 4989, pp. 322\u2013336. Springer, Heidelberg (2008)"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Claessen, K.: Shrinking and showing functions: (functional pearl). In: 5th ACM SIGPLAN Symposium on Haskell, pp. 73\u201380. ACM (2012)","DOI":"10.1145\/2430532.2364516"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-07151-0_2","volume-title":"Functional and Logic Programming","author":"K Claessen","year":"2014","unstructured":"Claessen, K., Dureg\u00e5rd, J., Pa\u0142ka, M.H.: Generating constrained random\u00a0data with\u00a0uniform\u00a0distribution. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 18\u201334. Springer, Heidelberg (2014)"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: 5th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 268\u2013279. ACM (2000)","DOI":"10.1145\/357766.351266"},{"key":"22_CR13","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. 2758, pp. 188\u2013203. Springer, Heidelberg (2003)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-31862-0_25","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"P Dybjer","year":"2005","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Random generators for dependent types. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 341\u2013355. Springer, Heidelberg (2005)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-662-46669-8_16","volume-title":"Programming Languages and Systems","author":"B Fetscher","year":"2015","unstructured":"Fetscher, B., Claessen, K., Pa\u0142ka, M., Hughes, J., Findler, R.B.: Making random judgments: automatically generating well-typed terms from the definition of a type-system. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 383\u2013405. Springer, Heidelberg (2015)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Fischer, S., Kuchen, H.: Systematic generation of glass-box test cases for functional logic programs. In: 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp. 63\u201374. ACM (2007)","DOI":"10.1145\/1273920.1273930"},{"issue":"2","key":"22_CR17","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reasoning 3(2), 95\u2013152 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"22_CR18","unstructured":"Haiyan, Q.: Testing and Proving in Dependent Type Theory. Ph.D. thesis, Chalmers (2003)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Hri\u0163cu, C., Hughes, J., Pierce, B.C., Spector-Zabusky, A., Vytiniotis, D., de Amorim, A.A., Lampropoulos, L.: Testing noninterference, quickly. In: 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 455\u2013468. ACM (2013)","DOI":"10.1145\/2500365.2500574"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69611-7_1","volume-title":"Practical Aspects of Declarative Languages","author":"J Hughes","year":"2007","unstructured":"Hughes, J.: QuickCheck testing for fun and profit. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 1\u201332. Springer, Heidelberg (2007)"},{"key":"22_CR21","unstructured":"Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (2006)"},{"issue":"1","key":"22_CR22","first-page":"41","volume":"2","author":"M Sozeau","year":"2009","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reasoning 2(1), 41\u201362 (2009)","journal-title":"J. Formalized Reasoning"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-35308-6_9","volume-title":"Certified Programs and Proofs","author":"P-N Tollitte","year":"2012","unstructured":"Tollitte, P.-N., Delahaye, D., Dubois, C.: Producing certified functional code from inductive specifications. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 76\u201391. Springer, Heidelberg (2012)"},{"key":"22_CR24","unstructured":"Wilson, S.: Supporting dependently typed functional programming with proof automation and testing. Ph.D. thesis, The University of Edinburgh, June 2011"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T14:24:38Z","timestamp":1676471078000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}