  In this article we present a tool for the verification of programs built on
top replicated databases. The tool evaluates a sequential specification and
deduces which operations need to be synchronized for the program to function
properly in a distributed environment. Our prototype is built over the
deductive verification platform Why3. The Why3 Framework provides a
sophisticated user experience, the possibility to scale to realistic case
studies, as well as a high degree of automation. A case study is presented and
discussed, with the purpose of experimentally validating our approach.
