6 citations · 17 across the 9 of their papers we have counts for
Showing 2022Show all
2 papers · 1 filter
cs.LO2022★ 1 cited
Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)
Pedro Barroso, Mário Pereira, António Ravara
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C. Considering…
cs.LO2022
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…