{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:10:53Z","timestamp":1746115853930,"version":"3.40.4"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906596"},{"type":"electronic","value":"9783031906602"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper introduces the QCheck-STM plugin for Ortac, a framework for dynamic verification of OCaml code. Ortac\/QCheck-STM consumes OCaml module signatures annotated with behavioural specification contracts expressed in the Gospel language, extracts a functional model of a mutable data structure from it, and generates code for automated runtime assertion checking. We report on the implementation of the tool, the structure of the generated code, and on errors found in established OCaml libraries.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_1","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:16Z","timestamp":1746005896000},"page":"3-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Dynamic Verification of OCaml Software with Gospel and Ortac\/QCheck-STM"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1616-0602","authenticated-orcid":false,"given":"Nikolaus","family":"Huber","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-1479-1574","authenticated-orcid":false,"given":"Naomi","family":"Spargo","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Osborne","sequence":"additional","affiliation":[]},{"given":"Samuel","family":"Hym","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6506-5468","authenticated-orcid":false,"given":"Jan","family":"Midtgaard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Artho, C., Gros, Q., Rousset, G., Banzai, K., Ma, L., Kitamura, T., Hagiya, M., Tanabe, Y., Yamamoto, M.: Model-Based API Testing of Apache ZooKeeper. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST). pp. 288\u2013298 (2017). https:\/\/doi.org\/10.1109\/ICST.2017.33","DOI":"10.1109\/ICST.2017.33"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Arts, T., Castro, L.M., Hughes, J.: Testing Erlang data types with Quviq QuickCheck. In: Proceedings of the 7th ACM SIGPLAN Workshop on Erlang, ERLANG\u201908. pp.\u00a01\u20138 (2008). https:\/\/doi.org\/10.1145\/1411273.1411275","DOI":"10.1145\/1411273.1411275"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Arts, T., Hughes, J., Johansson, J., Wiger, U.T.: Testing telecoms software with Quviq QuickCheck. In: Proceedings of the 2006 ACM SIGPLAN Workshop on Erlang. pp. 2\u201310 (2006). https:\/\/doi.org\/10.1145\/1159789.1159792","DOI":"10.1145\/1159789.1159792"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Arts, T., Hughes, J., Norell, U., Svensson, H.: Testing AUTOSAR software with QuickCheck. In: Eighth IEEE International Conference on Software Testing, Verification and Validation, ICST 2015 Workshops. pp.\u00a01\u20134 (2015). https:\/\/doi.org\/10.1109\/ICSTW.2015.7107466","DOI":"10.1109\/ICSTW.2015.7107466"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. pp. 49\u201369 (2005). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"1_CR6","unstructured":"Baudin, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language, http:\/\/frama-c.com\/download\/acsl.pdf"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Berghofer, S., Nipkow, T.: Random Testing in Isabelle\/HOL. In: SEFM. vol.\u00a04, pp. 230\u2013239 (2004). https:\/\/doi.org\/10.1109\/SEFM.2004.10049","DOI":"10.1109\/SEFM.2004.10049"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Bulwahn, L.: The New Quickcheck for Isabelle. In: Certified Programs and Proofs. pp. 92\u2013108 (2012). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_10","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A., Filli\u00e2tre, J.C., Louren\u00e7o, C., Pereira, M.: GOSPEL - Providing OCaml with a Formal Specification Language. In: FM 2019 - 23rd International Symposium on Formal Methods (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_29","DOI":"10.1007\/978-3-030-30942-8_29"},{"key":"1_CR10","unstructured":"Chargu\u00e9raud, A., Filli\u00e2tre, J.C., Pereira, M., Pottier, F.: VOCAL \u2013 A Verified OCAml Library (Sep 2017), https:\/\/inria.hal.science\/hal-01561094, ML Family Workshop 2017"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Claessen, K.: Shrinking and showing functions: (functional pearl). In: Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Haskell 2012. pp. 73\u201380 (2012). https:\/\/doi.org\/10.1145\/2364506.2364516","DOI":"10.1145\/2364506.2364516"},{"key":"1_CR12","doi-asserted-by":"publisher","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, ICFP\u201900. pp. 268\u2013279 (2000). https:\/\/doi.org\/10.1145\/351240.351266","DOI":"10.1145\/351240.351266"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Claessen, K., Hughes, J.: Testing monadic code with QuickCheck. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell 2002. pp. 65\u201377 (2002). https:\/\/doi.org\/10.1145\/581690.581696","DOI":"10.1145\/581690.581696"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Claessen, K., Palka, M.H., Smallbone, N., Hughes, J., Svensson, H., Arts, T., Wiger, U.T.: Finding race conditions in Erlang with QuickCheck and PULSE. In: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009. pp. 149\u2013160 (2009). https:\/\/doi.org\/10.1145\/1596550.1596574","DOI":"10.1145\/1596550.1596574"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Software Engineering and Formal Methods. pp. 233\u2013247 (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Combining Testing and Proving in Dependent Type Theory. In: Basin, D., Wolff, B. (eds.) Theorem Proving in Higher Order Logics. pp. 188\u2013203 (2003). https:\/\/doi.org\/10.1007\/10930755_12","DOI":"10.1007\/10930755_12"},{"key":"1_CR17","unstructured":"Filli\u00e2tre, J.C., Gondelman, L., Louren\u00e7o, C., Paskevich, A., Pereira, M., Melo\u00a0de Sousa, S., Walch, A.: A Toolchain to Produce Verified OCaml Libraries (Jan 2020), https:\/\/hal.science\/hal-01783851"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Pascutto, C.: Ortac: Runtime Assertion Checking for OCaml (Tool Paper). In: Runtime Verification: 21st International Conference, RV 2021, Proceedings. pp. 244\u2013253 (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_13","DOI":"10.1007\/978-3-030-88494-9_13"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 \u2014 Where Programs Meet Provers. In: Proceedings of the 22nd European Symposium on Programming. Lecture Notes in Computer Science, vol.\u00a07792, pp. 125\u2013128 (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Fink, G., Bishop, M.: Property-based testing: a new approach to testing for assurance. SIGSOFT Softw. Eng. Notes 22(4), 74\u201380 (1997). https:\/\/doi.org\/10.1145\/263244.263267","DOI":"10.1145\/263244.263267"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. pp. 234\u2013245. PLDI\u201902 (2002). https:\/\/doi.org\/10.1145\/512529.512558","DOI":"10.1145\/512529.512558"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Goodrich, M.T., Kloss, J.G.: Tiered Vectors: Efficient Dynamic Arrays for Rank-Based Sequences. In: Algorithms and Data Structures. pp. 205\u2013216 (1999). https:\/\/doi.org\/10.1007\/3-540-48447-7_21","DOI":"10.1007\/3-540-48447-7_21"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271\u2013281 (1972). https:\/\/doi.org\/10.1007\/BF00289507","DOI":"10.1007\/BF00289507"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Huber, N., Osborne, N., Hym, S., Midtgaard, J.: Dynamic Verification of OCaml Software with Gospel and Ortac\/QCheck-STM - Software Artifact (Oct 2024). https:\/\/doi.org\/10.5281\/zenodo.13988146","DOI":"10.5281\/zenodo.13988146"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Hughes, J.: Software testing with QuickCheck. In: Central European Functional Programming School - Third Summer School, CEFP 2009, Revised Selected Lectures. Lecture Notes in Computer Science, vol.\u00a06299, pp. 183\u2013223 (2009). https:\/\/doi.org\/10.1007\/978-3-642-17685-2_6","DOI":"10.1007\/978-3-642-17685-2_6"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Koopman, P.W.M., Plasmeijer, R.: Testing reactive systems with GAST. In: Revised Selected Papers from the Fourth Symposium on Trends in Functional Programming, TFP 2003. vol.\u00a04, pp. 111\u2013129 (2003)","DOI":"10.2307\/j.ctv36xvxxx.11"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Koopman, P.W.M., Plasmeijer, R.: Testing with functional reference implementations. In: Trends in Functional Programming - 11th International Symposium, TFP 2010. Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a06546, pp. 134\u2013149 (2010). https:\/\/doi.org\/10.1007\/978-3-642-22941-1_9","DOI":"10.1007\/978-3-642-22941-1_9"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (May 2006). https:\/\/doi.org\/10.1145\/1127878.1127884","DOI":"10.1145\/1127878.1127884"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Logic for Programming, Artificial Intelligence, and Reasoning. pp. 348\u2013370 (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"1_CR31","unstructured":"Mandrioli, D., Meyer, B., et\u00a0al.: Advances in object oriented software engineering. Prentice Hall (1992)"},{"key":"1_CR32","unstructured":"Midtgaard, J., Nicole, O., Osborne, N.: Multicoretests \u2014 Parallel testing libraries for OCaml 5.0. In: OCaml Users and Developers Workshop (2022), https:\/\/github.com\/ocaml-multicore\/multicoretests"},{"key":"1_CR33","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Automated Deduction - CADE-25. pp. 378\u2013388 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"1_CR34","unstructured":"Nilsson, R.: ScalaCheck: The Definitive Guide. Artima (2014)"},{"key":"1_CR35","unstructured":"Osborne, N., Pascutto, C.: Leveraging Formal Specifications to Generate Fuzzing Suites. In: OCaml Users and Developers Workshop (2021), https:\/\/inria.hal.science\/hal-03328646"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Palka, M.H., Claessen, K., Russo, A., Hughes, J.: Testing an optimising compiler by generating random lambda terms. In: Proceedings of the 6th International Workshop on Automation of Software Test. pp. 91\u201397. AST\u201911 (2011). https:\/\/doi.org\/10.1145\/1982595.1982615","DOI":"10.1145\/1982595.1982615"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Paraskevopoulou, Z., Hri\u0163cu, C., D\u00e9n\u00e8s, M., Lampropoulos, L., Pierce, B.C.: Foundational Property-Based Testing. In: ITP 2015 - 6th conference on Interactive Theorem Proving. Lecture Notes in Computer Science, vol.\u00a09236 (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_22","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"1_CR38","unstructured":"Pascutto, C.: Runtime verification of OCaml programs. Theses, Universit\u00e9 Paris-Saclay (Oct 2023), https:\/\/theses.hal.science\/tel-04696708"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Pereira, M., Ravara, A.: Cameleer: A deductive verification tool for OCaml. In: Computer Aided Verification. pp. 677\u2013689 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_31","DOI":"10.1007\/978-3-030-81688-9_31"},{"key":"1_CR40","unstructured":"Pottier, F.: Strong Automated Testing of OCaml Libraries. In: JFLA 2021 - 32es Journ\u00e9es Francophones des Langages Applicatifs (Feb 2021), https:\/\/inria.hal.science\/hal-03049511"},{"key":"1_CR41","doi-asserted-by":"publisher","unstructured":"Sergey, I.: Experience report: growing and shrinking polygons for random testing of computational geometry algorithms. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016. pp. 193\u2013199 (2016). https:\/\/doi.org\/10.1145\/2951913.2951927","DOI":"10.1145\/2951913.2951927"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Soares, T.L., Chirica, I., Pereira, M.: Static and dynamic verification of OCaml programs: The Gospel ecosystem (extended version) (2024), https:\/\/arxiv.org\/abs\/2407.17289","DOI":"10.1007\/978-3-031-75380-0_14"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F*. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016. pp. 256\u2013270 (2016). https:\/\/doi.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"The Coq development team: The Coq proof assistant (Jun 2024). https:\/\/doi.org\/10.5281\/zenodo.11551307","DOI":"10.5281\/zenodo.11551307"},{"key":"1_CR45","doi-asserted-by":"publisher","unstructured":"Tretmans, J.: Testing concurrent systems: A formal approach. In: CONCUR \u201999: Concurrency Theory, 10th International Conference, Proceedings. Lecture Notes in Computer Science, vol.\u00a01664, pp. 46\u201365 (1999). https:\/\/doi.org\/10.1007\/3-540-48320-9_6","DOI":"10.1007\/3-540-48320-9_6"},{"key":"1_CR46","unstructured":"Wikipedia: QuickCheck Wikipedia page (Accessed: 2024-10-06), https:\/\/en.wikipedia.org\/wiki\/QuickCheck"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:21Z","timestamp":1746005901000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","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":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}