Dynamic Verification of OCaml Software with ORTAC/QCheck-STM
In this talk I would like to introduce the QCheck-STM plugin for ORTAC, a framework for dynamic verification of OCaml code. ORTAC/QCheck-STM consumes OCaml module signatures annotated with contracts expressed in the Gospel language and generates code for automated runtime assertion checking from it. I will highlight some details of the implementation of the tool, the structure of the generated code, and on errors found in established OCaml libraries.
Speaker: Nikolaus Huber