Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Aktualności — Wydarzenia

SLIWOWICA

 

Cameleer: a Deductive Verification Tool for OCaml


Prelegent: Jacek Chrząszcz

2021-11-05 12:15

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.