2 citations · 4 across the 7 of their papers we have counts for
5 papers · 1 filter
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…
Cameleer: a Deductive Verification Tool for OCaml (extended version)
Mário Pereira, António Ravara
OCaml is particularly well-fitted for formal verification. On one hand, it is a multi-paradigm language with a well-defined semantics, allowing one to write clean, concise, type-sa…
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…
A Simple Functional Presentation and an Inductive Correctness Proof of the Horn Algorithm
António Ravara
We present a recursive formulation of the Horn algorithm for deciding the satisfiability of propositional clauses. The usual presentations in imperative pseudo-code are informal an…
Revisiting concurrent separation logic
Pedro Soares, António Ravara, Simão Melo de Sousa
We present a new soundness proof of Concurrent Separation Logic (CSL) based on a structural operational semantics (SOS). We build on two previous proofs and develop new auxiliary n…