6 citations · 17 across the 9 of their papers we have counts for
9 papers
A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)
Tiago Soares, Mário Pereira
Algebraic effects and handlers are a powerful abstraction to build non-local control-flow mechanisms such as resumable exceptions, lightweight threads, co-routines, generators, and…
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…
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…
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…
A coordination-free, convergent, and safe replicated tree
Sreeja Nair, Filipe Meirim, Mário Pereira +2
The tree is an essential data structure in many applications. In a distributed application, such as a distributed file system, the tree is replicated.To improve performance and ava…
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…