{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:50:40Z","timestamp":1740124240279,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T00:00:00Z","timestamp":1645488000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T00:00:00Z","timestamp":1645488000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-17-EURE-0002"],"award-info":[{"award-number":["ANR-17-EURE-0002"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2022,3]]},"DOI":"10.1007\/s11219-021-09572-z","type":"journal-article","created":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T09:04:01Z","timestamp":1645520641000},"page":"253-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards random and enumerative testing for OCaml and WhyML properties"],"prefix":"10.1007","volume":"30","author":[{"given":"Clotilde","family":"Erard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0990-9611","authenticated-orcid":false,"given":"Alain","family":"Giorgetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9rome","family":"Ricciardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,2,22]]},"reference":[{"key":"9572_CR1","unstructured":"Arndt, J. (2010). Matters Computational - Ideas, Algorithms, Source Code [The Fxtbook]. https:\/\/www.jjj.de\/fxt\/fxtpage.html"},{"key":"9572_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K., & Schulte, W. (2004). The spec# programming system: An overview. In: Proceedings of the International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS\u201904), Lecture Notes in Computer Science, vol. 3362, pp. 49\u201369. Springer-Verlag, Marseille, France","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"9572_CR3","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., & Schmitt, P. H. (eds.) (2007). Verification of Object-Oriented Software: The KeY Approach, Lecture Notes in Computer Science, vol. 4334. Springer, Heidelberg.","DOI":"10.1007\/978-3-540-69061-0"},{"key":"9572_CR4","doi-asserted-by":"publisher","unstructured":"Blatter, L., Kosmatov, N., Le\u00a0Gall, P., Prevosto, V., & Petiot, G. (2018). Static and dynamic verification of relational properties on self-composed C code. In: C.\u00a0Dubois, B.\u00a0Wolff (eds.) Tests and Proofs. TAP 2018, pp. 44\u201362. Springer International Publishing, Cham. https:\/\/doi.org\/10.1007\/978-3-319-21215-9_7","DOI":"10.1007\/978-3-319-21215-9_7"},{"key":"9572_CR5","doi-asserted-by":"publisher","unstructured":"Bulwahn, L. (2012). The new Quickcheck for Isabelle - random, exhaustive and symbolic testing under one roof. In: C.\u00a0Hawblitzel, D.\u00a0Miller (eds.) CPP 2012, Lecture Notes in Computer Science, vol. 7679, pp. 92\u2013108. Springer, Heidelberg, Kyoto, Japan. https:\/\/doi.org\/10.1007\/978-3-642-35308-6_10","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"9572_CR6","doi-asserted-by":"publisher","unstructured":"Claessen, K., & Hughes, J. (2000). 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.\u00a035, pp. 268\u2013279. ACM, New York. https:\/\/doi.org\/10.1145\/351240.351266","DOI":"10.1145\/351240.351266"},{"key":"9572_CR7","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Lecture Notes in Computer Science, vol. 2988, pp. 168\u2013176. Springer. https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"9572_CR8","doi-asserted-by":"crossref","unstructured":"Correnson, L. (2014). Qed. Computing what remains to be proved. In: J.M. Badger, K.Y. Rozier (eds.) NFM 2014, Lecture Notes in Computer Science, vol. 8430, pp. 215\u2013229. Springer, Heidelberg. http:\/\/dx.doi.org\/10.1007\/978-3-319-06200-6_17","DOI":"10.1007\/978-3-319-06200-6_17"},{"key":"9572_CR9","unstructured":"Dijkstra, E. W. (1976). A Discipline of Programming. In: Series in Automatic Computation. Prentice Hall."},{"key":"9572_CR10","doi-asserted-by":"publisher","unstructured":"Dubois, C., & Giorgetti, A. (2018). Tests and proofs for custom data generators. Formal Aspects of Computing 30(6), 659\u2013684. https:\/\/doi.org\/10.1007\/s00165-018-0459-1","DOI":"10.1007\/s00165-018-0459-1"},{"key":"9572_CR11","doi-asserted-by":"publisher","unstructured":"Dubois, C., Giorgetti, A., & Genestier, R. (2016). Tests and proofs for enumerative combinatorics. In: K.B. Aichernig, A.C. Furia (eds.) Tests and Proofs. TAP 2016, Lecture Notes in Computer Science, vol. 6792, pp. 57\u201375. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-41135-4_4","DOI":"10.1007\/978-3-319-41135-4_4"},{"key":"9572_CR12","doi-asserted-by":"publisher","unstructured":"Dureg\u00e5rd, J., Jansson, P., & Wang, M. (2012). Feat: functional enumeration of algebraic types. In: Proceedings of the 2012 Haskell Symposium, ACM SIGPLAN Notices, vol.\u00a047, pp. 61\u201372. Association for Computing Machinery, New York, NY, USA. https:\/\/doi.org\/10.1145\/2364506.2364515","DOI":"10.1145\/2364506.2364515"},{"key":"9572_CR13","doi-asserted-by":"publisher","unstructured":"Erard, C., & Giorgetti, A. (2019). Bounded exhaustive testing with certified and optimized data enumeration programs. In: Testing Software and Systems. ICTSS 2019., Lecture Notes in Computer Science, vol. 11812, pp. 159\u2013175. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-030-31280-0_10","DOI":"10.1007\/978-3-030-31280-0_10"},{"key":"9572_CR14","unstructured":"Filli\u00e2tre, J. -C., & Pereira, M. (2016) It\u00e9rer avec confiance. In: Journ\u00e9es Francophones des Langages Applicatifs. JFLA. https:\/\/hal.inria.fr\/hal-01240891"},{"key":"9572_CR15","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J. -C., & Pereira, M. (2016). A modular way to reason about iteration. In: S.\u00a0Rayadurgam, O.\u00a0Tkachuk (eds.) NFM 2016, Lecture Notes in Computer Science, vol. 9690, pp. 322\u2013336. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-40648-0_24","DOI":"10.1007\/978-3-319-40648-0_24"},{"key":"9572_CR16","unstructured":"Fitinghoff, N. (2019). Extraction of Rust code from the Why3 verification platform. Ph.D. thesis, Lule\u00e5 University of Technology. http:\/\/www.diva-portal.org\/smash\/get\/diva2:1303268\/FULLTEXT02#page20"},{"key":"9572_CR17","doi-asserted-by":"crossref","unstructured":"Genestier, R., Giorgetti, A., & Petiot, G. (2015). Sequential generation of structured arrays and its deductive verification. In: J.C. Blanchette, N.\u00a0Kosmatov (eds.) Tests and Proofs. TAP 2015, Lecture Notes in Computer Science, vol. 9154, pp. 109\u2013128. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-21215-9_7","DOI":"10.1007\/978-3-319-21215-9_7"},{"key":"9572_CR18","unstructured":"Giorgetti, A., Dubois, C., & Lazarini, R. (2019). Combinatoire formelle avec Why3 et Coq. In: N.\u00a0Magaud, Z.\u00a0Dargaye (eds.) Journ\u00e9es Francophones des Langages Applicatifs. JFLA 2019., pp. 139\u2013154. https:\/\/hal.inria.fr\/hal-01985195"},{"key":"9572_CR19","unstructured":"Giorgetti, A., & Lazarini, R. (2018). Preuve de programmes d\u2019\u00e9num\u00e9ration avec Why3. In: AFADL 2018, pp. 14\u201319. http:\/\/afadl2018.ls2n.fr\/wp-content\/uploads\/sites\/38\/2018\/06\/AFADL_Procs_2018.pdf"},{"key":"9572_CR20","doi-asserted-by":"crossref","unstructured":"Hauzar, D., March\u00e9, C., & Moy, Y. (2016). Counterexamples from proof failures in SPARK. In: R.\u00a0De\u00a0Nicola, E.\u00a0K\u00fchn (eds.) Software Engineering and Formal Methods. SEFM 2016, Lecture Notes in Computer Science, vol. 9763, pp. 215\u2013233. Springer, Cham. https:\/\/hal.inria.fr\/hal-01314885","DOI":"10.1007\/978-3-319-41591-8_15"},{"key":"9572_CR21","doi-asserted-by":"crossref","unstructured":"Herdt, V., Gro\u00dfe, D., Le, H. M., & Drechsler, R. (2019). Verifying instruction set simulators using coverage-guided fuzzing(*). In: J.\u00a0Teich, F.\u00a0Fummi (eds.) Design, Automation & Test in Europe Conference & Exhibition, DATE 2019, Florence, Italy, March 25-29, 2019, pp. 360\u2013365. IEEE.\u00a0https:\/\/doi.org\/10.23919\/DATE.2019.8714912","DOI":"10.23919\/DATE.2019.8714912"},{"key":"9572_CR22","unstructured":"Knuth, D. E. (1997). The Art of Computer Programming, Volume 1 (3rd Ed.): Fundamental Algorithms. Addison Wesley Longman Publishing Co., Inc., USA."},{"key":"9572_CR23","doi-asserted-by":"crossref","unstructured":"Kosmatov, N., March\u00e9, C., Moy, Y., & Signoles, J. (2016). Static versus dynamic verification in Why3, Frama-C and SPARK 2014. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Lecture Notes in Computer Science, vol. 9952, pp. 461\u2013478. Springer and Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-47166-2_32","DOI":"10.1007\/978-3-319-47166-2_32"},{"key":"9572_CR24","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"GT Leavens","year":"1999","unstructured":"Leavens, G. T., Baker, A. L., & Ruby, C. (1999). JML: A notation for detailed design. In H. Kilov, B. Rumpe, & I. Simmonds (Eds.), Behavioral Specifications of Businesses and Systems (pp. 175\u2013188). Boston: Kluwer Academic Publishers."},{"key":"9572_CR25","unstructured":"Leino, K. R. M., & Moskal, M. (2010). Usable auto-active verification. In: Usable Verification Workshop. http:\/\/fm.csl.sri.com\/UV10\/"},{"key":"9572_CR26","doi-asserted-by":"crossref","unstructured":"Midtgaard, J., & M\u00f8ller, A. (2017). QuickChecking static analysis properties. Software Testing, Verification and Reliability 27(6), e1640. https:\/\/onlinelibrary.wiley.com\/doi\/abs\/10.1002\/stvr.1640","DOI":"10.1002\/stvr.1640"},{"key":"9572_CR27","unstructured":"Nelson, J. (2017). The design and use of QuickCheck. Blog post https:\/\/begriffs.com\/posts\/2017-01-14-design-use-quickcheck.html"},{"key":"9572_CR28","doi-asserted-by":"publisher","unstructured":"Padhye, R., Lemieux, C., & Sen, K. (2019). JQF: Coverage-guided property-based testing in Java. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, pp. 398\u2013401. Association for Computing Machinery, New York, NY, USA. https:\/\/doi.org\/10.1145\/3293882.3339002","DOI":"10.1145\/3293882.3339002"},{"key":"9572_CR29","unstructured":"Pereira, M. J. P. (2018) Tools and techniques for the verification of modular stateful code. Ph.D. thesis, Universit\u00e9 Paris-Sud. https:\/\/tel.archives-ouvertes.fr\/tel-01980343\/document"},{"key":"9572_CR30","doi-asserted-by":"publisher","unstructured":"Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., & Julliand, J. (2018). How testing helps to diagnose proof failures. Formal Aspects of Computing 30(6), 629\u2013657. https:\/\/doi.org\/10.1007\/s00165-018-0456-4","DOI":"10.1007\/s00165-018-0456-4"},{"key":"9572_CR31","unstructured":"Rebours, N. (2019). An introduction to fuzzing OCaml with AFL, Crowbar and Bun.\u00a0https:\/\/tarides.com\/blog\/2019-09-04-an-introduction-to-fuzzing-ocaml-with-afl-crowbar-and-bun"},{"key":"9572_CR32","doi-asserted-by":"publisher","unstructured":"Reich, J. S., Naylor, M., & Runciman, C. (2013). Advances in Lazy SmallCheck. In: R.\u00a0Hinze (ed.) Implementation and Application of Functional Languages. IFL 2012., Lecture Notes in Computer Science, vol. 8241, pp. 53\u201370. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-41582-1_4","DOI":"10.1007\/978-3-642-41582-1_4"},{"key":"9572_CR33","unstructured":"Rieu-Helft, R. (2018). Un m\u00e9canisme d\u2019extraction vers C pour Why3. In: Journ\u00e9es Francophones des Langages Applicatifs. JFLA 2018., pp. 203\u2013209. https:\/\/hal.inria.fr\/hal-01707376v1"},{"key":"9572_CR34","doi-asserted-by":"publisher","unstructured":"Runciman, C., Naylor, M., & Lindblad, F. (2008). SmallCheck and Lazy SmallCheck - automatic exhaustive testing for small values. In: Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, pp. 37\u201348. ACM. https:\/\/doi.org\/10.1145\/1411286.1411292","DOI":"10.1145\/1411286.1411292"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-021-09572-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-021-09572-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-021-09572-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,22]],"date-time":"2022-04-22T10:12:13Z","timestamp":1650622333000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-021-09572-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,22]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,3]]}},"alternative-id":["9572"],"URL":"https:\/\/doi.org\/10.1007\/s11219-021-09572-z","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"type":"print","value":"0963-9314"},{"type":"electronic","value":"1573-1367"}],"subject":[],"published":{"date-parts":[[2022,2,22]]},"assertion":[{"value":"13 September 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}