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 条

[1] Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
Taube, Marcelo
Losa, Giuliano
McMillan, Kenneth L.
Padon, Oded
Sagiv, Mooly
Shoham, Sharon
Wilcox, James R.
Woos, Doug
ACM SIGPLAN NOTICES, 2018, 53 (04) : 662 - 677
[2] Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
Taube, Marcelo
Losa, Giuliano
McMillan, Kenneth L.
Padon, Oded
Sagiv, Mooly
Shoham, Sharon
Wilcox, James R.
Woos, Doug
PROCEEDINGS OF THE 39TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, PLDI 2018, 2018, : 662 - 677
[3] Deductive verification of distributed groupware systems
Imine, A
Molli, P
Oster, G
Rusinowitch, M
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 226 - 240
[4] Deductive verification of modular systems
Finkbeiner, B
Manna, Z
Sipma, HB
COMPOSITIONALITY: THE SIGNIFICANT DIFFERENCE, 1998, 1536 : 239 - 275
[5] Deductive verification of alternating systems
Slanina, Matteo
Sipma, Henny B.
Manna, Zohar
FORMAL ASPECTS OF COMPUTING, 2008, 20 (4-5) : 507 - 560
[6] Deductive probabilistic verification methods of safety, liveness and nonzenoness for distributed real-time systems
Yamane, S
EMBEDDED SOFTWARE AND SYSTEMS, PROCEEDINGS, 2005, 3820 : 332 - 345
[7] Deductive verification of telecommunication systems written in C
Anureev I.S.
Automatic Control and Computer Sciences, 2013, 47 (7) : 413 - 419
[8] Deductive verification of hybrid systems using STeP
Manna, Z
Sipma, HB
HYBRID SYSTEMS: COMPUTATION AND CONTROL, 1998, 1386 : 305 - 318
[9] Deductive Verification of Distributed Protocols in First-Order Logic
Padon, Oded
PROCEEDINGS OF THE 2018 18TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), 2018, : 3 - 3
[10] Verification of distributed applications
Langenstein, Bruno
Nonnengart, Andreas
Rock, Georg
Stephan, Werner
COMPUTER SAFETY, RELIABILITY, AND SECURITY, PROCEEDINGS, 2007, 4680 : 315 - +

← 1 2 3 4 5 →