6 citations · 17 across the 9 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2020★ 1 cited
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…
cs.PL2020★ 6 cited
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…