6 citations · 9 across the 3 of their papers we have counts for
6 papers
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…
CISE3: Verifying Weakly Consistent Applications with Why3
Filipe Meirim, Mário Pereira, Carla Ferreira
In this paper we present a tool for the formal analysis of applications built on top of replicated databases, where data integrity can be at stake. To address this issue, one can i…
WhylSon: Proving your Michelson Smart Contracts in Why3
Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira +1
This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a fo…
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…
Desfuncionalizar para Provar
Mário Pereira
This paper explores the idea of using defunctionalization as a proof technique for higher-order programs. Defunctionalization builds on substituting functional values by a first-or…