{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:42:49Z","timestamp":1770835369606,"version":"3.50.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816872","type":"print"},{"value":"9783030816889","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present , an automated deductive verification tool for OCaml. We leverage on the recently proposed GOSPEL (Generic OCaml SPEcification Language) to attach rigorous, yet readable, behavioral specification to OCaml code. The formally-specified program is fed to our toolchain, which translates it into an equivalent one in WhyML, the programming and specification language of the Why3 verification framework. We report on successful case studies conducted in .<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_31","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"677-689","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Cameleer: A Deductive Verification Tool for OCaml"],"prefix":"10.1007","author":[{"given":"M\u00e1rio","family":"Pereira","sequence":"first","affiliation":[]},{"given":"Ant\u00f3nio","family":"Ravara","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"31_CR1","doi-asserted-by":"publisher","unstructured":"Ahman, D., et al.: Dijkstra monads for free. In: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 515\u2013529. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009878","DOI":"10.1145\/3009837.3009878"},{"key":"31_CR2","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging Rust Types for Modular Specification and Verification. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360573","DOI":"10.1145\/3360573"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3"},{"key":"31_CR4","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 418\u2013430 (2011). https:\/\/doi.org\/10.1145\/2034773.2034828","DOI":"10.1145\/2034773.2034828"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-030-30942-8_29","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"A Chargu\u00e9raud","year":"2019","unstructured":"Chargu\u00e9raud, A., Filli\u00e2tre, J.-C., Louren\u00e7o, C., Pereira, M.: GOSPEL\u2014providing OCaml with a formal specification language. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 484\u2013501. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_29"},{"key":"31_CR6","unstructured":"Chargu\u00e9raud, A., Filli\u00e2tre, J.C., Pereira, M., Pottier, F.: VOCAL - A Verified OCAml Library. In: ML Family Workshop (2017). https:\/\/hal.inria.fr\/hal-01561094"},{"issue":"3","key":"31_CR7","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s10817-017-9431-7","volume":"62","author":"A Chargu\u00e9raud","year":"2017","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reason. 62(3), 331\u2013365 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9431-7","journal-title":"J. Autom. Reason."},{"key":"31_CR8","unstructured":"Claret, G.: Program in Coq. (Programmer en Coq). Ph.D. thesis, Paris Diderot University, France (2018). https:\/\/tel.archives-ouvertes.fr\/tel-01890983"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Dailler, S., March\u00e9, C., Moy, Y.: Lightweight interactive proving inside an automatic program verifier. In: 4th Workshop on Formal Integrated Development Environment (F-IDE) (2018)","DOI":"10.4204\/EPTCS.284.1"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/978-3-319-96145-3_33","volume-title":"Computer Aided Verification","author":"M Eilers","year":"2018","unstructured":"Eilers, M., M\u00fcller, P.: Nagini: a static verifier for python. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 596\u2013603. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_33"},{"issue":"5","key":"31_CR11","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-011-0211-0","volume":"13","author":"JC Filli\u00e2tre","year":"2011","unstructured":"Filli\u00e2tre, J.C.: Deductive software verification. Int. J. Softw. Tools Technol. Transf. (STTT) 13(5), 397\u2013403 (2011). https:\/\/doi.org\/10.1007\/s10009-011-0211-0","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C.: Simpler proofs with decentralized invariants. J. Log. Algebraic Methods Program. (2020, to appear). https:\/\/hal.inria.fr\/hal-02518570","DOI":"10.1016\/j.jlamp.2021.100645"},{"key":"31_CR13","unstructured":"Filli\u00e2tre, J.C., et al.: A toolchain to produce verified OCaml libraries. Research report, Universit\u00e9 Paris-Saclay (2020). https:\/\/hal.archives-ouvertes.fr\/hal-01783851"},{"key":"31_CR14","unstructured":"Filli\u00e2tre, J.C., Gondelman, L., Paskevich, A.: A pragmatic type system for deductive verification. Research report, Universit\u00e9 Paris Sud (2016). https:\/\/hal.archives-ouvertes.fr\/hal-01256434v3"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_21"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-030-61362-4_7","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"J-C Filli\u00e2tre","year":"2020","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Abstraction and genericity in Why3. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 122\u2013142. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_7"},{"key":"31_CR18","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":"31_CR19","doi-asserted-by":"publisher","unstructured":"Gu\u00e9neau, A., Jourdan, J., Chargu\u00e9raud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, (ITP). LIPIcs, vol. 141, pp. 18:1\u201318:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.18","DOI":"10.4230\/LIPIcs.ITP.2019.18"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"issue":"3","key":"31_CR21","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"31_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-319-17524-9_2","volume-title":"NASA Formal Methods","author":"V Kuncak","year":"2015","unstructured":"Kuncak, V.: Developing verified software using leon. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 12\u201315. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_2"},{"key":"31_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"31_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"31_CR25","doi-asserted-by":"publisher","unstructured":"Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-1-84628-692-6","DOI":"10.1007\/978-1-84628-692-6"},{"key":"31_CR26","unstructured":"Pereira, M., Ravara, A.: Cameleer: a deductive verification tool for OCaml. CoRR (2021). https:\/\/arxiv.org\/abs\/2104.11050"},{"key":"31_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-70594-9_17","volume-title":"Mathematics of Program Construction","author":"Y R\u00e9gis-Gianas","year":"2008","unstructured":"R\u00e9gis-Gianas, Y., Pottier, F.: A hoare logic for call-by-value functional programs. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 305\u2013335. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70594-9_17"},{"key":"31_CR28","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, pp. 55\u201374. IEEE Computer Society, USA (2002)"},{"key":"31_CR29","doi-asserted-by":"publisher","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Gupta, R., Amarasinghe, S.P. (eds.) 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 159\u2013169. ACM (2008). https:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"issue":"9","key":"31_CR30","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709\u2013720 (1998). https:\/\/doi.org\/10.1109\/32.713327","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"31_CR31","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2160910.2160911","volume":"34","author":"J Smans","year":"2012","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2:1\u20132:58 (2012). https:\/\/doi.org\/10.1145\/2160910.2160911","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"31_CR32","unstructured":"The Why3 Development Team: The Why3 platform, version 1.3.3. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay (2020). http:\/\/why3.lri.fr\/manual.pdf"},{"key":"31_CR33","doi-asserted-by":"publisher","unstructured":"Vazou, N., Breitner, J., Kunkel, R., Horn, D.V., Hutton, G.: Theorem proving for all: equational reasoning in liquid haskell (functional pearl). In: Wu, N. (ed.) 11th ACM SIGPLAN International Symposium on Haskell, pp. 132\u2013144. ACM (2018). https:\/\/doi.org\/10.1145\/3242744.3242756","DOI":"10.1145\/3242744.3242756"},{"key":"31_CR34","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Jones, S.L.P.: Refinement types for haskell. In: Jeuring, J., Chakravarty, M.M.T. (eds.) 19th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 269\u2013282. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81688-9_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:27:56Z","timestamp":1626452876000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"290","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":"63","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":"0","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":"22% - 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":"12","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":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}