6 citations · 10 across the 5 of their papers we have counts for
3 papers · 1 filter
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…