CISE3：基于 Why3 的弱一致性应用验证
编程语言
2019-09-10 v1 计算机科学中的逻辑
摘要
在本文中，我们提出了一个用于验证构建于复制数据库之上的程序的工具。该工具评估顺序规范，并推导出程序在分布式环境中正常运行所需同步的操作。我们的原型构建于演绎验证平台 Why3 之上。Why3 框架提供了精细的用户体验、扩展到现实案例研究的可能性，以及高度的自动化。我们给出并讨论了一个案例研究，以实验性地验证我们的方法。
引用
@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}
}
备注
Article in Portuguese, accepted in the national informatics conference INForum 2019