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

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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2019-09
Main Authors: Meirim, Filipe, Pereira, Mário, Ferreira, Carla
Format: Article
Language:English
Subjects:
Case studies
Program verification (computers)
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422