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 条

[21] Decidability of opacity verification problems in labeled Petri net systems
Tong, Yin
Li, Zhiwu
Seatzu, Carla
Giua, Alessandro
AUTOMATICA, 2017, 80 : 48 - 53
[22] Deductive software verification
Filliâtre J.-C.
International Journal on Software Tools for Technology Transfer, 2011, 13 (5) : 397 - 403
[23] Reliability and Confidentiality Co-Verification for Parallel Applications in Distributed Systems
Xie, Guoqi
Yang, Kehua
Luo, Haibo
Li, Renfa
Hu, Shiyan
IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 2021, 32 (06) : 1353 - 1368
[24] RULE ALLOCATION IN DISTRIBUTED DEDUCTIVE DATABASE-SYSTEMS
MOHANIA, MK
SARDA, NL
DATA & KNOWLEDGE ENGINEERING, 1994, 14 (02) : 117 - 141
[25] A Hybrid Fragmentation Approach for Distributed Deductive Database Systems
Seung-Jin Lim
Yiu-Kai Ng
Knowledge and Information Systems, 2001, 3 (2) : 198 - 224
[26] Vertical fragmentation and allocation in distributed deductive database systems
Lim, SJ
Ng, YK
INFORMATION SYSTEMS, 1997, 22 (01) : 1 - 24
[27] Scalability and Precision by Combining Expressive Type Systems and Deductive Verification
Lanzinger, Florian
Weigl, Alexander
Ulbrich, Mattias
Dietl, Werner
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5 (OOPSLA):
[28] Deductive verification of real-time systems using STeP
Bjorner, NS
Manna, Z
Sipma, HB
Uribe, TE
THEORETICAL COMPUTER SCIENCE, 2001, 253 (01) : 27 - 60
[29] Deductive verification of real-time systems using STeP
Bjorner, NS
Manna, Z
Sipma, HB
Uribe, TE
TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, 1997, 1231 : 22 - 43
[30] INCREMENTAL PROTOCOL VERIFICATION USING DEDUCTIVE DATABASE-SYSTEMS
LIAO, IE
LIU, MT
PROCEEDINGS : FIFTH INTERNATIONAL CONFERENCE ON DATA ENGINEERING, 1989, : 216 - 223

← 1 2 3 4 5 →