Modularity for decidability of deductive verification with applications to distributed systems

被引：22

作者：

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

共 46 条

[1]

Alberti F., Ghilardi S., Pagani E., Counting constraints in flat array fragments, Automated Reasoning. Springer, Cham, pp. 65-81, (2016)

[2]

Bakst A., Von Gleissenthall K., Gokhan Kici R., Jhala R., Verifying distributed programs via canonical sequentialization, PACMPL 1, OOPSLA (2017), pp. 1101-11027, (2017)

[3]

Berdine J., Calcagno C., O'Hearn P.W., A decidable fragment of separation logic, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings., pp. 97-109, (2004)

[4]

Bertot Y., Casteran P., Interactive Theorem Proving and Program Development-coq'Art: The Calculus of Inductive Constructions, (2004)

[5]

Bloem R., Jacobs S., Khalimov A., Konnov I., Rubin S., Veith H., Widder J., Decidability of Parameterized Verification, (2015)

[6]

Bradley A.R., Manna Z., Sipma H.B., What's decidable about arrays?, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings., pp. 427-442, (2006)

[7]

Chand S., Liu Y.A., Stoller S.D., Formal verification of multi-paxos for distributed consensus, FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings 21. Springer, pp. 119-136, (2016)

[8]

Chaudhuri K., Doligez D., Lamport L., Merz S., The tla+proof system: Building a heterogeneous verification platform, Proceedings of the 7th International Colloquium Conference on Theoretical Aspects of Computing (ICTAC'10). Springer-Verlag, (2010)

[9]

Cohen E., Dahlweid M., Hillebrand M.A., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S., Vcc: A practical system for verifying concurrent c, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Lecture Notes in Computer Science), 5674, pp. 23-42, (2009)

[10]

Etcd: A Highly-available Key Value Store for Shared Configuration and Service Discovery, (2014)

← 1 2 3 4 5 →