CISE3: Verifica\c{c}\~ao de aplica\c{c}\~oes com consist\^encia fraca em Why3

TL;DR

This paper introduces CISE3, a tool integrated with Why3 for verifying distributed database applications with weak consistency, focusing on identifying necessary synchronization to ensure correct operation.

Contribution

It presents a novel verification tool that analyzes distributed database programs to determine synchronization needs, leveraging the Why3 platform for automation and scalability.

Findings

Successfully validated the approach with a case study

Demonstrated the tool's ability to handle realistic scenarios

Showed effectiveness in identifying synchronization requirements

Abstract

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.