{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:01:01Z","timestamp":1725858061437},"publisher-location":"Cham","reference-count":31,"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_4","type":"book-chapter","created":{"date-parts":[[2016,6,20]],"date-time":"2016-06-20T16:23:38Z","timestamp":1466439818000},"page":"57-75","source":"Crossref","is-referenced-by-count":3,"title":["Tests and Proofs for Enumerative Combinatorics"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Dubois","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Genestier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,21]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Cuellar, J., Liu, Z. (eds.) Software Engineering and Formal Methods (SEFM 2004), pp. 230\u2013239. IEEE Computer Society (2004)","DOI":"10.1109\/SEFM.2004.1347524"},{"key":"4_CR2","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, New York (2004)"},{"key":"4_CR3","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)"},{"issue":"8","key":"4_CR4","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1016\/j.comgeo.2010.06.006","volume":"45","author":"C Brun","year":"2012","unstructured":"Brun, C., Dufourd, J., Magaud, N.: Designing and proving correct a convex hull algorithm with hypermaps in Coq. Comput. Geom. 45(8), 436\u2013457 (2012)","journal-title":"Comput. Geom."},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 - Random, exhaustive and symbolic testing under one roof. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92\u2013108. Springer, Heidelberg (2012)"},{"key":"4_CR6","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: Constraint Reasoning in FOCALTEST. In: International Conference on Software and Data Technologies (ICSOFT 2010), Athens, July 2010"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Not., vol. 35, pp. 268\u2013279. ACM, New York (2000)","DOI":"10.1145\/351240.351266"},{"issue":"2","key":"4_CR8","first-page":"9","volume":"1","author":"C Dubois","year":"2007","unstructured":"Dubois, C., Mota, J.M.: Geometric modeling with B: formal specification of generalized maps. J. Sci. Pract. Comput. 1(2), 9\u201324 (2007)","journal-title":"J. Sci. Pract. Comput."},{"issue":"11","key":"4_CR9","doi-asserted-by":"crossref","first-page":"2974","DOI":"10.1016\/j.patcog.2007.02.013","volume":"40","author":"J Dufourd","year":"2007","unstructured":"Dufourd, J.: Design and formal proof of a new optimal image segmentation program with hypermaps. Pattern Recogn. 40(11), 2974\u20132993 (2007)","journal-title":"Pattern Recogn."},{"issue":"2\u20133","key":"4_CR10","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/j.tcs.2008.02.012","volume":"403","author":"J Dufourd","year":"2008","unstructured":"Dufourd, J.: Polyhedra genus theorem and Euler formula: a hypermap-formalized intuitionistic proof. Theor. Comput. Sci. 403(2\u20133), 133\u2013159 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"4_CR11","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/s10817-009-9117-x","volume":"43","author":"J Dufourd","year":"2009","unstructured":"Dufourd, J.: An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps. J. Autom. Reasoning 43(1), 19\u201351 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"4_CR13","first-page":"646","volume":"7","author":"JR Edmonds","year":"1960","unstructured":"Edmonds, J.R.: A combinatorial representation for oriented polyhedral surfaces. Notices Amer. Math. Soc. 7, 646 (1960)","journal-title":"Notices Amer. Math. Soc."},{"key":"4_CR14","unstructured":"Giorgetti, A., Senni, V.: Specification and Validation of Algorithms Generating Planar Lehman Words, June 2012. https:\/\/hal.inria.fr\/hal-00753008"},{"key":"4_CR15","unstructured":"Gonthier, G.: A computer checked proof of the Four Colour Theorem (2005). http:\/\/research.microsoft.com\/gonthier\/4colproof.pdf"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Computer Mathematics","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, pp. 333\u2013333. Springer, Heidelberg (2008)"},{"key":"4_CR17","unstructured":"Hritcu, C., Lampropoulos, L., D\u00e9n\u00e8s, M., Paraskevopoulou, Z.: Randomized property-based testing plugin for Coq. https:\/\/github.com\/QuickChick"},{"key":"4_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-17333-2","volume-title":"Patterns in Permutations and Words","author":"S Kitaev","year":"2011","unstructured":"Kitaev, S.: Patterns in Permutations and Words. Springer, New York (2011)"},{"key":"4_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-38361-1","volume-title":"Graphs on Surfaces and Their Applications","author":"SK Lando","year":"2004","unstructured":"Lando, S.K., Zvonkin, A.K.: Graphs on Surfaces and Their Applications. Springer, New York (2004)"},{"key":"4_CR20","unstructured":"Lazarus, F.: Combinatorial graphs and surfaces from the computational and topological viewpoint followed by some notes on the isometric embedding of the square flat torus (2014). http:\/\/www.gipsa-lab.grenoble-inp.fr\/~francis.lazarus\/Documents\/hdr-Lazarus.pdf"},{"key":"4_CR21","unstructured":"Mathematical Components team: Library mathcomp.ssreflect.fingraph. http:\/\/math-comp.github.io\/math-comp\/htmldoc\/mathcomp.ssreflect.fingraph.html"},{"key":"4_CR22","unstructured":"Owre, S.: Random testing in PVS. In: Workshop on Automated Formal Methods (AFM) (2006)"},{"key":"4_CR23","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.) ITP 2015. LNCS, vol. 9236, pp. 325\u2013343. Springer, Heidelberg (2015)"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM\/IEEE Conference on Supercomputing, Supercomputing 1991, pp. 4\u201313. ACM, New York (1991)","DOI":"10.1145\/125826.125848"},{"key":"4_CR25","unstructured":"Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. In: Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, Haskell 2008, Victoria, BC, Canada, 25 September 2008, pp. 37\u201348 (2008). http:\/\/doi.acm.org\/10.1145\/1411286.1411292"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1007\/978-3-662-46669-8_33","volume-title":"Programming Languages and Systems","author":"EL Seidel","year":"2015","unstructured":"Seidel, E.L., Vazou, N., Jhala, R.: Type targeted testing. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 812\u2013836. Springer, Heidelberg (2015)"},{"key":"4_CR27","unstructured":"Senni, V.: Validation library. https:\/\/subversion.assembla.com\/svn\/validation\/"},{"key":"4_CR28","unstructured":"SWI: Prolog. http:\/\/www.swi-prolog.org\/"},{"key":"4_CR29","unstructured":"The OEIS Foundation Inc: The On-Line Encyclopedia of Integer Sequences. https:\/\/oeis.org\/A000698"},{"key":"4_CR30","first-page":"309","volume-title":"New Directions in the Theory of Graphs: Proceedings","author":"WT Tutte","year":"1973","unstructured":"Tutte, W.T.: What is a map? In: Harary, F. (ed.) New Directions in the Theory of Graphs: Proceedings, pp. 309\u2013325. Academic Press, New York (1973)"},{"issue":"5","key":"4_CR31","doi-asserted-by":"crossref","first-page":"986","DOI":"10.4153\/CJM-1979-091-3","volume":"31","author":"WT Tutte","year":"1979","unstructured":"Tutte, W.T.: Combinatorial oriented maps. Canad. J. Math. 31(5), 986\u20131004 (1979)","journal-title":"Canad. J. Math."}],"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_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:44:31Z","timestamp":1498322671000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41135-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319411347","9783319411354"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41135-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}