CISE3: Verificação de aplicações com consistência fraca em Why3

09/09/2019
by   Filipe Meirim, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset