CISE3: Verifying Weakly Consistent Applications with Why3

TL;DR

This paper introduces CISE3, a tool built on Why3 for formally analyzing and verifying the correct synchronization points in distributed applications to ensure data integrity without sacrificing system availability.

Contribution

The paper presents a novel tool that automates the reasoning about optimal synchronization in replicated database applications using deductive verification.

Findings

Successfully verified several case studies.

Automated deduction of necessary synchronization points.

Improved reasoning about data integrity in distributed systems.

Abstract

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.