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 条

[31] Motion planning for metamorphic systems: Feasibility, decidability, and distributed reconfiguration
Dumitrescu, A
Suzuki, I
Yamashita, M
IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, 2004, 20 (03): : 409 - 418
[32] Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems
Chatain, Thomas
Gastin, Paul
Sznajder, Nathalie
SOFSEM 2009-THEORY AND PRACTICE OF COMPUTER SCIENCE, PROCEEDINGS, 2009, 5404 : 141 - 152
[33] VERIFICATION OF DISTRIBUTED SYSTEMS - AN EXPERIMENT
VERGAMINI, D
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 386 : 249 - 259
[34] VERIFICATION OF DISTRIBUTED SYSTEMS - AN EXPERIMENT
VERGAMINI, D
FORMAL PROPERTIES OF FINITE AUTOMATA AND APPLICATIONS, 1989, 386 : 249 - 259
[35] Deductive Verification of Hybrid Control Systems Modeled in Simulink with KeYmaera X
Liebrenz, Timm
Herber, Paula
Glesner, Sabine
FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018, 2018, 11232 : 89 - 105
[36] Deductive Verification of Legacy Code
Beckert, Bernhard
Bormer, Thorsten
Grahl, Daniel
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I, 2016, 9952 : 749 - 765
[37] Deductive verification of cryptographic software
Almeida, Jose Bacelar
Barbosa, Manuel
Pinto, Jorge Sousa
Vieira, Barbara
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (03) : 203 - 218
[38] Is there a future for deductive temporal verification?
Dixon, Clare
Fisher, Michael
Konev, Boris
TIME 2006: THIRTEENTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2006, : 11 - +
[39] Deductive Verification with Ghost Monitors
Clochard, Martin
Marche, Claude
Paskevich, Andrei
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
[40] The Decidability of Verification under PS 2.0
Abdulla, Parosh Aziz
Atig, Mohamed Faouzi
Godbole, Adwait
Krishna, S.
Vafeiadis, Viktor
PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2021, 2021, 12648 : 1 - 29

← 1 2 3 4 5 →