Cameleer: a Deductive Verification Tool for OCaml

Prelegent(ci)

Jacek Chrząszcz

Afiliacja

MIMUW

Termin

5 listopada 2021 12:15

Pokój

p. 5820

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Despite all the advances in deductive verification and proof automation over the past few decades, little attention has been given to the family of functional languages. We present Cameleer, a tool for the deductive verification of programs written in OCaml, with a clear focus on proof automation. Cameleer uses the recently proposed GOSPEL (Generic OCaml SPEcification Language) to attach rigorous, yet readable, behavioral specification to OCaml code.

---