ICFP 2021
Sun 22 - Sat 28 August 2021
Thu 26 Aug 2021 18:30 - 19:00 at ML - Semantics & Verification Chair(s): Martin Elsman

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.

** Note to ML workshop organizers: given our tool clearly targets verification of OCaml programs, we feel this could also be of interest for the OCaml workshop. However, we believe a deductive verification tool for programs written in an important language of the ML family can interest a wider audience, hence we are submitting to the ML workshop in the first place.

Extended abstract (main.pdf)352KiB
Talk (talk.pdf)1.24MiB

Thu 26 Aug

Displayed time zone: Seoul change

18:00 - 19:30
Semantics & VerificationML at ML
Chair(s): Martin Elsman University of Copenhagen, Denmark
18:00
30m
Talk
Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming
ML
Daniel Hillerström The University of Edinburgh
Pre-print Media Attached
18:30
30m
Talk
Cameleer: a Deductive Verification Tool for OCaml
ML
Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS
File Attached
19:00
30m
Talk
Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques
ML
Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Trinity College Dublin, Nikos Tzevelekos Queen Mary University of London
File Attached