Modularity for decidability of deductive verification with applications to distributed systems

被引：21

作者：

Taube M. ^{[1
]}

Losa G. ^{[2
]}

McMillan K.L. ^{[3
]}

Padon O. ^{[1
]}

Sagiv M. ^{[1
]}

Shoham S. ^{[1
]}

Wilcox J.R. ^{[4
]}

Woos D. ^{[4
]}

机构：

[1] Taube, Marcelo

[2] Losa, Giuliano

[3] McMillan, Kenneth L.

[4] Padon, Oded

[5] Sagiv, Mooly

[6] Shoham, Sharon

[7] Wilcox, James R.

[8] Woos, Doug

来源：

| 2018年 / Association for Computing Machinery, 2 Penn Plaza, Suite 701, New York, NY 10121-0701, United States卷 / 53期

基金：

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

关键词：

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

D O I：

10.1145/3192366.3192414

中图分类号：

学科分类号：

摘要：

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. © 2018 ACM.

引用

页码：662 / 677

页数：15

共 50 条

[41] On the decidability of shared memory consistency verification
Sezgin, A
Gopalakrishnan, G
Third ACM & IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2005, : 199 - 208
[42] VERIFICATION DECIDABILITY OF PRESBURGER ARRAY PROGRAMS
SUZUKI, N
JEFFERSON, D
JOURNAL OF THE ACM, 1980, 27 (01) : 191 - 205
[43] Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains
Biscaia, M.
Henriques, D.
Mateus, P.
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2015, 16 (01)
[44] FORMAL SPECIFICATION AND VERIFICATION OF DISTRIBUTED SYSTEMS
CHEN, BS
YEH, RT
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1983, 9 (06) : 710 - 722
[45] COMPOSITIONAL SPECIFICATION AND VERIFICATION OF DISTRIBUTED SYSTEMS
JONSSON, B
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (02): : 259 - 303
[46] Automatic verification for a class of distributed systems
G. Manduchi
M. Moro
Distributed Computing, 2000, 13 : 127 - 143
[47] Automatic verification for a class of distributed systems
Manduchi, G
Moro, M
DISTRIBUTED COMPUTING, 2000, 13 (03) : 127 - 143
[48] Heterogeneous analysis and verification for distributed systems
Steffen, B
Margaria, T
Classen, A
SOFTWARE-CONCEPTS AND TOOLS, 1996, 17 (01): : 13 - 25
[49] Verification of Liveness Properties in Distributed Systems
Yadav, Divakar
Butler, Michael
CONTEMPORARY COMPUTING, PROCEEDINGS, 2009, 40 : 625 - +
[50] A combination of explicit and deductive knowledge with branching time: Completeness and decidability results
Lomuscio, Alessio
Wozna, Bozena
DECLARATIVE AGENT LANGUAGES AND TECHNOLOGIES III, 2006, 3904 : 188 - 204

← 1 2 3 4 5 →