Auto-active Verification of Graph Algorithms, Written in OCaml

Daniel Castanho, Mário Pereira

Functional programming offers the perfect ground for building correct-by-construction software. Languages of such paradigm normally feature state-of-the-art type systems, good abst…