CISE3: Verifica\c{c}\~ao de aplica\c{c}\~oes com consist\^encia fraca em Why3
Programming Languages
2019-09-10 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1909.03721,
title = {CISE3: Verifica\c{c}\~ao de aplica\c{c}\~oes com consist\^encia fraca em Why3},
author = {Filipe Meirim and Mário Pereira and Carla Ferreira},
journal= {arXiv preprint arXiv:1909.03721},
year = {2019}
}
Comments
Article in Portuguese, accepted in the national informatics conference INForum 2019