@inproceedings{33ec2ad7915d452c96a89f3c049992a8,
title = "Cameleer: A Deductive Verification Tool for OCaml",
abstract = "We present Cameleer, 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 Cameleer.",
keywords = "Deductive software verification, GOSPEL, OCaml, Why3",
author = "M{\'a}rio Pereira and Ant{\'o}nio Ravara",
note = "info:eu-repo/grantAgreement/EC/H2020/897873/EU# info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F04516%2F2020/PT# ; 33rd International Conference on Computer Aided Verification, CAV 2021 ; Conference date: 20-07-2021 Through 23-07-2021",
year = "2021",
doi = "10.1007/978-3-030-81688-9_31",
language = "English",
isbn = "978-3-030-81687-2",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "677--689",
editor = "Alexandra Silva and Leino, {K. Rustan}",
booktitle = "Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings",
address = "Netherlands",
}