I4: incremental inference of inductive invariants for verification of distributed protocols
I4: incremental inference of inductive invariants for verification of distributed protocols
复制标题
I4：用于验证分布式协议的归纳不变量的增量推理
DOI：
10.1145/3341301.3359651
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Sakallah, Karem A.
中科院分区：
文献类型：
--
作者：
Ma, Haojun;Goel, Aman;Jeannin, Jean-Baptiste;Kapritsos, Manos;Kasikci, Baris;Sakallah, Karem A.
正确设计和实现分布式系统是一项非常具有挑战性的任务。近年来，形式化验证已被成功地用于证明分布式系统的正确性。形式验证的核心是一个具有归纳不变量的计算机检查证明。然而，找到这个归纳不变量是证明中最困难的部分。遗憾的是，目前的证明技术需要开发人员手工地、费力地找到归纳不变量，本文提出了一种新的方法，归纳不变量的增量推理（I4），用于自动生成分布式协议的归纳不变量。我们的思想的本质很简单：协议的一个有限实例的归纳不变量可以用来推断无限分布式协议的一般归纳不变量。在I4中，我们创建协议的有限实例;使用模型检查工具自动导出此有限实例的归纳不变量;并将此不变量推广为无限协议的归纳不变量。我们的实验表明，I4可以证明几个分布式协议的正确性，如Chord，2 PC和事务链，几乎没有人的努力。
Designing and implementing distributed systems correctly is a very challenging task. Recently, formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computer-checked proof with an inductive invariant. Finding this inductive invariant, however, is the most difficult part of the proof. Alas, current proof techniques require inductive invariants to be found manually---and painstakingly---by the developer.In this paper, we present a new approach,Incremental Inference of Inductive Invariants(I4), to automatically generate inductive invariants for distributed protocols. The essence of our idea is simple: the inductive invariant of afiniteinstance of the protocol can be used to infer a general inductive invariant for theinfinitedistributed protocol. In I4, we create a finite instance of the protocol; use a model checking tool to automatically derive the inductive invariant for this finite instance; and generalize this invariant to an inductive invariant for the infinite protocol. Our experiments show that I4 can prove the correctness of several distributed protocols like Chord, 2PC and Transaction Chains with little to no human effort.
登录
查看更多内容
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor
Verilog RTL 设计中基于 IC3 的模型检查技术的实证评估
DOI：
--
发表时间：
2019
期刊：
Design, Automation and Test in Europe
影响因子：
--
作者：
Aman Goel;K. Sakallah
通讯作者：
K. Sakallah
影响因子：
22.7
作者：
LIPTON, RJ
通讯作者：
LIPTON, RJ
通用不变量的属性导向推理或证明它们的不存在
DOI：
--
发表时间：
2015
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
Aleksandr Karbyshev;Nikolaj S. Bjørner;Shachar Itzhaky;N. Rinetzky;Sharon Shoham
通讯作者：
Sharon Shoham
使用具有语法引导抽象的 IC3 对 Verilog RTL 进行模型检查
影响因子：
7.4
作者：
Aman Goel;K. Sakallah
通讯作者：
K. Sakallah