1 citations · 1 across the 1 of their papers we have counts for
2 papers
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.LO2020
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
Pedro Barroso, Mário Pereira, António Ravara
We present an approach to obtain formally verified implementations of classical Computational Logic algorithms. We choose the Why3 platform because it allows to implement functions…