{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:24:16Z","timestamp":1743125056595,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030312794"},{"type":"electronic","value":"9783030312800"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-31280-0_10","type":"book-chapter","created":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T23:06:50Z","timestamp":1570489610000},"page":"159-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Bounded Exhaustive Testing with Certified and Optimized Data Enumeration Programs"],"prefix":"10.1007","author":[{"given":"Clotilde","family":"Erard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"10_CR1","unstructured":"QuviQ testing tools (2019). http:\/\/www.quviq.com"},{"key":"10_CR2","first-page":"440","volume-title":"Matters Computational","author":"J\u00f6rg Arndt","year":"2010","unstructured":"Arndt, J.: Matters Computational - Ideas, Algorithms, Source Code [The fxtbook] (2010). https:\/\/www.jjj.de\/fxt\/fxtpage.html"},{"key":"10_CR3","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Melquiond, G., Paskevich, A.: The Why3 Platform (2018). http:\/\/why3.lri.fr\/manual.pdf"},{"key":"10_CR4","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 - 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). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_10"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.jlamp.2018.05.003","volume":"99","author":"S Dailler","year":"2018","unstructured":"Dailler, S., Hauzar, D., March\u00e9, C., Moy, Y.: Instrumenting a weakest precondition calculus for counterexample generation. J. Logic Algebraic Methods Program. 99, 97\u2013113 (2018). https:\/\/doi.org\/10.1016\/j.jlamp.2018.05.003","journal-title":"J. Logic Algebraic Methods Program."},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1007\/s00165-018-0459-1","volume":"30","author":"C Dubois","year":"2018","unstructured":"Dubois, C., Giorgetti, A.: Tests and proofs for custom data generators. Formal Aspects Comput. 30, 659\u2013684 (2018)","journal-title":"Formal Aspects Comput."},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-319-41135-4_4","volume-title":"Tests and Proofs","author":"C Dubois","year":"2016","unstructured":"Dubois, C., Giorgetti, A., Genestier, R.: Tests and proofs for enumerative combinatorics. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 57\u201375. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41135-4_4"},{"key":"10_CR8","unstructured":"Filli\u00e2tre, J.-C., Pereira, M.: It\u00e9rer avec confiance. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2016) (2016). https:\/\/hal.inria.fr\/hal-01240891"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-319-40648-0_24","volume-title":"NASA Formal Methods","author":"J-C Filli\u00e2tre","year":"2016","unstructured":"Filli\u00e2tre, J.-C., Pereira, M.: A modular way to reason about iteration. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 322\u2013336. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_24"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-319-21215-9_7","volume-title":"Tests and Proofs","author":"R Genestier","year":"2015","unstructured":"Genestier, R., Giorgetti, A., Petiot, G.: Sequential generation of structured arrays and its deductive verification. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 109\u2013128. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21215-9_7"},{"key":"10_CR11","unstructured":"Giorgetti, A., Lazarini, R.: Preuve de programmes d\u2019\u00e9num\u00e9ration avec Why3. In: AFADL 2018, pp. 14\u201319 (2018). http:\/\/afadl2018.ls2n.fr\/wp-content\/uploads\/sites\/38\/2018\/06\/AFADL_Procs_2018.pdf"},{"key":"10_CR12","unstructured":"Giorgetti, A., Dubois, C., Lazarini, R.: Combinatoire formelle avec Why3 et Coq. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2019), Les Rousses, France, pp. 139\u2013154, January 2019. https:\/\/hal.inria.fr\/hal-01985195"},{"key":"10_CR13","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formaliz. Reason. 3, 95\u2013152 (2010)","journal-title":"J. Formaliz. Reason."},{"key":"10_CR14","unstructured":"Hri\u0163cu, C., Lampropoulos, L., D\u00e9n\u00e8s, M., Paraskevopoulou, Z.: QuickChick: randomized property-based testing plugin for Coq (2018). https:\/\/github.com\/QuickChick\/QuickChick"},{"issue":"7","key":"10_CR15","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1109\/32.538605","volume":"22","author":"D Jackson","year":"1996","unstructured":"Jackson, D., Damon, C.: Elements of style: analyzing a software design feature with a counterexample detector. IEEE Trans. Softw. Eng. 22(7), 484\u2013495 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR16","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Usable Verification Workshop (2010). http:\/\/fm.csl.sri.com\/UV10\/"},{"issue":"7","key":"10_CR17","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Hri\u0163cu, 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, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_22"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-319-72308-2_6","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"R Rieu-Helft","year":"2017","unstructured":"Rieu-Helft, R., March\u00e9, C., Melquiond, G.: How to get an efficient yet verified arbitrary-precision integer library. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 84\u2013101. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72308-2_6"},{"key":"10_CR20","doi-asserted-by":"publisher","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, pp. 37\u201348. ACM (2008). https:\/\/doi.org\/10.1145\/1411286.1411292","DOI":"10.1145\/1411286.1411292"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Sullivan, K.J., Yang, J., Coppit, D., Khurshid, S., Jackson, D.: Software assurance by bounded exhaustive testing. In: Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, pp. 133\u2013142. ACM (2004)","DOI":"10.1145\/1007512.1007531"}],"container-title":["Lecture Notes in Computer Science","Testing Software and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31280-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,13]],"date-time":"2024-03-13T20:58:52Z","timestamp":1710363532000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-31280-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030312794","9783030312800"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31280-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"8 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"IFIP International Conference on Testing Software and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"pts2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ictss2019.centralesupelec.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2,1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}