Modularity for Decidability of Deductive Verification with Applications to Distributed Systems

被引：0

作者：

Taube, Marcelo ^{[1
]}

Losa, Giuliano ^{[2
]}

McMillan, Kenneth L. ^{[3
]}

Padon, Oded ^{[1
]}

Sagiv, Mooly ^{[1
]}

Shoham, Sharon ^{[1
]}

Wilcox, James R. ^{[4
]}

Woos, Doug ^{[4
]}

机构：

[1] Tel Aviv Univ, Tel Aviv, Israel

[2] UCLA, Los Angeles, CA USA

[3] Microsoft Res, Redmond, WA USA

[4] Univ Washington, Seattle, WA 98195 USA

来源：

PROCEEDINGS OF THE 39TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, PLDI 2018 | 2018年

基金：

欧洲研究理事会; 欧盟地平线“2020”; 美国国家科学基金会;

关键词：

Formal verification; Modularity; Decidable logic; Ivy; Distributed systems; Paxos; Raft; FORMAL VERIFICATION;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Proof automation can substantially increase productivity in formal verification of complex systems. However, unpredictablility of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. We propose to solve this problem not by improving the provers, but by using a modular proof methodology that allows us to produce decidable verification conditions. Decidability greatly improves predictability of proof automation, resulting in a more practical verification approach. We apply this methodology to develop verified implementations of distributed protocols, demonstrating its effectiveness.

引用

页码：662 / 677

页数：16

共 46 条

[1] Counting Constraints in Flat Array Fragments [J].

Alberti, Francesco ;

Ghilardi, Silvio ;

Pagani, Elena .

AUTOMATED REASONING (IJCAR 2016), 2016, 9706 :65-81

[2] Verifying distributed programs via canonical sequentialization [J].

Bakst, Alexander ;

Gleissenthall, Klaus V. ;

Kici, Rami Gökhan ;

Jhala, Ranjit .

Proceedings of the ACM on Programming Languages, 2017, 1 (OOPSLA)

[3]

Berdine J, 2004, LECT NOTES COMPUT SC, V3328, P97

[4]

Bertot Y., 2004, TEXT THEORET COMP S

[5]

Bloem R., 2015, DECIDABILITY PARAMET, DOI DOI 10.2200/S00658ED1V01Y201508DCT013

[6]

Bradley AR, 2006, LECT NOTES COMPUT SC, V3855, P427

[7] Formal Verification of Multi-Paxos for Distributed Consensus [J].

Chand, Saksham ;

Liu, Yanhong A. ;

Stoller, Scott D. .

FM 2016: FORMAL METHODS, 2016, 9995 :119-136

[8]

Chaudhuri K, 2010, LECT NOTES COMPUT SC, V6255, P44, DOI 10.1007/978-3-642-14808-8_3

[9]

Cohen E, 2009, LECT NOTES COMPUT SC, V5674, P23, DOI 10.1007/978-3-642-03359-9_2

[10]

CoreOS, 2014, etcd: A highly-available key value store for shared configuration and service discovery

← 1 2 3 4 5 →