Showing cs.LOShow all
2 papers · 1 filter
cs.LO2024
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…
cs.LO2024
Practical Deductive Verification of OCaml Programs (Extended Version)
Mário Pereira
In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in OCaml. In particular, we show how one can use the GOSPEL…