Cameleer: A Deductive Verification Tool for OCaml

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
EditorsAlexandra Silva, K. Rustan Leino
Place of PublicationCham
PublisherSpringer
Pages677-689
Number of pages13
ISBN (Electronic)978-3-030-81688-9
ISBN (Print)978-3-030-81687-2
DOIs
Publication statusPublished - 2021
Event33rd International Conference on Computer Aided Verification, CAV 2021 - Virtual, Online
Duration: 20 Jul 202123 Jul 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume12760 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference33rd International Conference on Computer Aided Verification, CAV 2021
CityVirtual, Online
Period20/07/2123/07/21

Keywords

  • Deductive software verification
  • GOSPEL
  • OCaml
  • Why3

Fingerprint

Dive into the research topics of 'Cameleer: A Deductive Verification Tool for OCaml'. Together they form a unique fingerprint.

Cite this