{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:38Z","timestamp":1780994798686,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466681","type":"print"},{"value":"9783662466698","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":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46669-8_33","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T18:37:37Z","timestamp":1427913457000},"page":"812-836","source":"Crossref","is-referenced-by-count":35,"title":["Type Targeted Testing"],"prefix":"10.1007","author":[{"given":"Eric L.","family":"Seidel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: ICSE 2004: Software Engineering, pp. 326\u2013335 (2004)","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: ISSTA 2002: Software Testing and Analysis, pp. 123\u2013133. ACM (2002)","DOI":"10.1145\/566171.566191"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Claessen, K., Dureg\u00e5rd, J., Palka, M.H.: Generating constrained random data with uniform distribution. In: FLOPS 2014, pp. 18\u201334 (2014)","DOI":"10.1007\/978-3-319-07151-0_2"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of haskell programs. In: ICFP. ACM (2000)","DOI":"10.1145\/351240.351266"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n\u2019 crash: combining static checking and testing. In: ICSE, pp. 422\u2013431 (2005)","DOI":"10.1145\/1062455.1062533"},{"key":"33_CR6","unstructured":"Neto, A.C.D., Subramanyan, R., Vieira, M., Travassos, G.H.: A survey on model-based testing approaches: A systematic review. In: WEASELTech 2007. ACM (2007)"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Dunfield, J.: Refined typechecking with Stardust. In: PLPV (2007)","DOI":"10.1145\/1292597.1292602"},{"key":"33_CR8","unstructured":"Erk\u00f6k, L.: SBV: SMT based verification in haskell, http:\/\/leventerkok.github.io\/sbv\/"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: OOPSLA, pp. 1\u201315 (2001)","DOI":"10.1145\/504311.504283"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Gill, A., Runciman, C.: Haskell program coverage. In: Haskell 2007. ACM (2007)","DOI":"10.1145\/1291201.1291203"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: PLDI, pp. 213\u2013223 (2005)","DOI":"10.1145\/1064978.1065036"},{"issue":"2","key":"33_CR13","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"33_CR14","first-page":"151","volume-title":"POPL 2012","author":"A.S. K\u00f6ksal","year":"2012","unstructured":"K\u00f6ksal, A.S., Kuncak, V., Suter, P.: Constraints as control. In: POPL 2012, pp. 151\u2013164. ACM, New York (2012)"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Magalh\u00e3es, J.P., Dijkstra, A., Jeuring, J., L\u00f6h, A.: A generic deriving mechanism for haskell. In: Haskell Symposium. ACM (2010)","DOI":"10.1145\/1863523.1863529"},{"key":"33_CR16","unstructured":"Marick, B.: How to misuse code coverage. In: Proceedings of the 16th Interational Conference on Testing Computer Software, pp. 16\u201318 (1999)"},{"key":"33_CR17","unstructured":"Marinov, D., Khurshid, S.: Testera: A novel framework for automated testing of java programs. In: ASE 2001. IEEE Computer Society, Washington, DC (2001)"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"33_CR19","unstructured":"Nelson, G.: Techniques for program verification. Tech. Rep. CSL81-10, Xerox Palo Alto Research Center (1981)"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Nystrom, N., Saraswat, V.A., Palsberg, J., Grothoff, C.: Constrained types for object-oriented languages. In: OOPSLA, pp. 457\u2013474 (2008)","DOI":"10.1145\/1449955.1449800"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: Automatic exhaustive testing for small values. In: Haskell Symposium. ACM (2008)","DOI":"10.1145\/1411286.1411292"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: A concolic unit testing engine for c. In: ESEC\/FSE. ACM (2005)","DOI":"10.21236\/ADA482657"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P.-Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: ICFP (2011)","DOI":"10.1145\/2034773.2034811"},{"key":"33_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N. Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013white box test generation for.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"33_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-37036-6_13","volume-title":"Programming Languages and Systems","author":"N. Vazou","year":"2013","unstructured":"Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 209\u2013228. Springer, Heidelberg (2013)"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R.: Liquidhaskell: Experience with refinement types in the real world. In: Haskell Symposium (2014)","DOI":"10.1145\/2633357.2633366"},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for haskell. In: ICFP (2014)","DOI":"10.1145\/2628136.2628161"},{"key":"33_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-78917-8_2","volume-title":"Formal Methods and Testing","author":"M. Veanes","year":"2008","unstructured":"Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-based testing of object-oriented reactive systems with spec explorer. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol.\u00a04949, pp. 39\u201376. Springer, Heidelberg (2008)"},{"key":"33_CR29","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI (1998)","DOI":"10.1145\/277650.277732"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46669-8_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T20:24:10Z","timestamp":1747859050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46669-8_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466681","9783662466698"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46669-8_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}