{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:00:59Z","timestamp":1725858059156},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319411347"},{"type":"electronic","value":"9783319411354"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-41135-4_3","type":"book-chapter","created":{"date-parts":[[2016,6,20]],"date-time":"2016-06-20T16:23:38Z","timestamp":1466439818000},"page":"37-56","source":"Crossref","is-referenced-by-count":2,"title":["Advances in Property-Based Testing for $$\\alpha $$ Prolog"],"prefix":"10.1007","author":[{"given":"James","family":"Cheney","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Pessina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,21]]},"reference":[{"issue":"3","key":"3_CR1","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.entcs.2006.06.017","volume":"176","author":"D Aspinall","year":"2007","unstructured":"Aspinall, D., Beringer, L., Momigliano, A.: Optimisation validation. Electron. Notes Theor. Comput. Sci. 176(3), 37\u201359 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-540-73595-3_28","volume-title":"Automated Deduction \u2013 CADE-21","author":"D Baelde","year":"2007","unstructured":"Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.F.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 391\u2013397. Springer, Heidelberg (2007)"},{"key":"3_CR3","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0743-1066(90)90023-X","volume":"8","author":"R Barbuti","year":"1990","unstructured":"Barbuti, R., Mancarella, P., Pedreschi, D., Turini, F.: A transformational approach to negation in logic programming. J. Log. Program. 8, 201\u2013228 (1990)","journal-title":"J. Log. Program."},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"JC 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. 6989, pp. 12\u201327. Springer, Heidelberg (2011)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC 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. 6172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Weber, T., Batty, M., Owens, S., Sarkar, S.: Nitpicking C++ concurrency. In: Schneider-Kamp, P., Hanus, M. (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pp. 113\u2013124. ACM (2011)","DOI":"10.1145\/2003476.2003493"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Breitner, J.: Formally proving a compiler transformation safe. In: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, Haskell 2015, pp. 35\u201346. ACM, New York (2015)","DOI":"10.1145\/2804302.2804312"},{"issue":"3","key":"3_CR8","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/s10817-009-9164-3","volume":"45","author":"J Cheney","year":"2010","unstructured":"Cheney, J.: Equivariant unification. J. Autom. Reasoning 45(3), 267\u2013300 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Cheney, J., Momigliano, A.: Mechanized metatheory model-checking. In: Leuschel, M., Podelski, A. (eds.) PPDP, pp. 75\u201386. ACM (2007)","DOI":"10.1145\/1273920.1273931"},{"key":"3_CR10","unstructured":"Cheney, J., Momigliano, A., Pessina, M.: Appendix to Advances in property-based testing for $$\\alpha $$ Prolog (2016). http:\/\/momigliano.di.unimi.it\/alphaCheck.html"},{"issue":"5","key":"3_CR11","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/1387673.1387675","volume":"30","author":"J Cheney","year":"2008","unstructured":"Cheney, J., Urban, C.: Nominal logic programming. ACM Trans. Program. Lang. Syst. 30(5), 26 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), pp. 268\u2013279. ACM (2000)","DOI":"10.1145\/351240.351266"},{"key":"3_CR13","volume-title":"Semantics Engineering with PLT Redex","author":"M Felleisen","year":"2009","unstructured":"Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. The MIT Press, Massachusetts (2009)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"1","key":"3_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0743-1066(93)90007-4","volume":"17","author":"J Harland","year":"1993","unstructured":"Harland, J.: Success and failure for hereditary Harrop formulae. J. Log. Program. 17(1), 1\u201329 (1993)","journal-title":"J. Log. Program."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Heath, Q., Miller, D.: A framework for proof certificates in finite state exploration. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, 2\u20133 Aug 2015, vol. 186. EPTCS, pp. 11\u201326 (2015)","DOI":"10.4204\/EPTCS.186.4"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Hritcu, C., Hughes, J., Pierce, B.C., Spector-Zabusky, A., Vytiniotis, D., Azevedo de Amorim, A., Lampropoulos, L.: Testing noninterference, quickly. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp. 455\u2013468. ACM, New York (2013)","DOI":"10.1145\/2500365.2500574"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J.A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run your research: on the effectiveness of lightweight mechanization. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 285\u2013296. ACM, New York (2012)","DOI":"10.1145\/2103656.2103691"},{"issue":"3","key":"3_CR19","first-page":"301","volume":"3","author":"J-L Lassez","year":"1987","unstructured":"Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reasoning 3(3), 301\u2013318 (1987)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"3_CR20","first-page":"409","volume":"1","author":"J Leach","year":"2001","unstructured":"Leach, J., Nieva, S., Rodr\u00edguez-Artalejo, M.: Constraint logic programming with hereditary Harrop formulas. TPLP 1(4), 409\u2013445 (2001)","journal-title":"TPLP"},{"issue":"7","key":"3_CR21","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107\u2013115 (2009)","journal-title":"CACM"},{"issue":"2","key":"3_CR22","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284\u2013304 (2009)","journal-title":"Inf. Comput."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Loveland, W.D., Nadathur, G.: Proof procedures for logic programming. Technical report, Durham, NC, USA (1994)","DOI":"10.1007\/978-3-642-51136-3_14"},{"issue":"1","key":"3_CR24","first-page":"100","volume":"10","author":"WM McKeeman","year":"1998","unstructured":"McKeeman, W.M.: Differential testing for software. Digit. Tech. J. 10(1), 100\u2013107 (1998)","journal-title":"Digit. Tech. J."},{"issue":"4","key":"3_CR25","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321\u2013358 (1992)","journal-title":"J. Symb. Comput."},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-44622-2_28","volume-title":"Computer Science Logic","author":"A Momigliano","year":"2000","unstructured":"Momigliano, A.: Elimination of negation in a logical framework. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, p. 411. Springer, Heidelberg (2000)"},{"issue":"4","key":"3_CR27","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1145\/937555.937559","volume":"4","author":"A Momigliano","year":"2003","unstructured":"Momigliano, A., Pfenning, F.: Higher-order pattern complement and the strict lambda-calculus. ACM Trans. Comput. Log. 4(4), 493\u2013529 (2003)","journal-title":"ACM Trans. Comput. Log."},{"key":"3_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics-with Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics-with Isabelle\/HOL. Springer, Heidelberg (2014)"},{"key":"3_CR29","unstructured":"Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM) (2006)"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Palka, M.H., Claessen, K., Russo, A., Hughes, J.: Testing an optimising compiler by generating random lambda terms. In: AST 2011, pp. 91\u201397. ACM (2011)","DOI":"10.1145\/1982595.1982615"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/978-3-319-22102-1_22","volume-title":"Interactive Theorem Proving","author":"Z Paraskevopoulou","year":"2015","unstructured":"Paraskevopoulou, Z., Hritcu, C., D\u00e9n\u00e8s, M., Lampropoulos, L., Pierce, B.C.: Foundational property-based testing. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving. LNCS, vol. 9236, pp. 325\u2013343. Springer, Heidelberg (2015)"},{"key":"3_CR32","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"183","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 183, 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"issue":"2","key":"3_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-8(2:14)2012","volume":"8","author":"C Urban","year":"2012","unstructured":"Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in nominal Isabelle. Log. Methods Comput. Sci. 8(2), 1\u201335 (2012)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2\u20133","key":"3_CR34","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D Volpano","year":"1996","unstructured":"Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2\u20133), 167\u2013187 (1996)","journal-title":"J. Comput. Secur."},{"issue":"3","key":"3_CR35","doi-asserted-by":"crossref","first-page":"22:1","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1\u201322:50 (2013)","journal-title":"J. ACM"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in c compilers. In: PLDI 2011, pp. 283\u2013294. ACM, New York (2011)","DOI":"10.1145\/1993498.1993532"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41135-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,18]],"date-time":"2023-08-18T23:33:56Z","timestamp":1692401636000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41135-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319411347","9783319411354"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41135-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}