论文标题
CISE3：用Why3验证弱一致的应用程序
CISE3: Verifying Weakly Consistent Applications with Why3
论文作者
论文摘要
在本文中，我们介绍了一个工具，用于对在复制数据库之上构建的应用程序进行正式分析，其中数据完整性可能受到威胁。为了解决此问题，可以在系统中引入同步。在太多地方引入同步可能会损害系统的可用性，但是如果在很少的地方引入，则数据完整性可能会受到损害。我们工具的目的是帮助程序员理由有关系统中同步的正确平衡。我们的工具分析了一个顺序规范，并推论哪些操作需要同步，以便程序在分布式环境中安全执行。我们的原型建立在演绎验证平台Why3之上，Why3提供了友好且集成的用户体验。使用我们的工具成功验证了一些案例研究。
In this paper we present a tool for the formal analysis of applications built on top of replicated databases, where data integrity can be at stake. To address this issue, one can introduce synchronization in the system. Introducing synchronization in too many places can hurt the system's availability but if introduced in too few places, then data integrity can be compromised. The goal of our tool is to aid the programmer reason about the correct balance of synchronization in the system. Our tool analyses a sequential specification and deduces which operations require synchronization in order for the program to safely execute in a distributed environment. Our prototype is built on top of the deductive verification platform Why3, which provides a friendly and integrated user experience. Several case studies have been successfully verified using our tool.
