Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)

Tiago Lopes Soares, Ion Chirica, Mário Pereira

We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specificat…