2 papers
cs.PL2025
Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
Ion Chirica, Mário Pereira
Albeit being a central notion of every programming language, formally and modularly reasoning about iteration proves itself to be a non-trivial feat, specially in the context of hi…
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…