CISE3: Verifying Weakly Consistent Applications with Why3

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 introduce synchronization in the system. Introducing synchronization in too many places can hurt the system's availability but if introduced in too few places, then data integrity can be compromised. The goal of our tool is to aid the programmer reason about the correct balance of synchronization in the system. Our tool analyses a sequential specification and deduces which operations require synchronization in order for the program to safely execute in a distributed environment. Our prototype is built on top of the deductive verification platform Why3, which provides a friendly and integrated user experience. Several case studies have been successfully verified using our tool.