%0 Conference Proceedings
%T On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency
%+ Humboldt State University (HSU)
%A Völlinger, Kim
%A Akili, Samira
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 38th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Madrid, Spain
%Y Christel Baier
%Y Luís Caires
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-10854
%P 161-180
%8 2018-06-18
%D 2018
%R 10.1007/978-3-319-92612-4_9
%K Certification
%K Distributed algorithm
%K Formal instance verification
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X A major problem in software engineering is assuring the correctness of a distributed system. A certifying distributed algorithm (CDA) computes for its input-output pair (i, o) an additional witness w – a formal argument for the correctness of (i, o). Each CDA features a witness predicate such that if the witness predicate holds for a triple (i, o, w), the input-output pair (i, o) is correct. An accompanying checker algorithm decides the witness predicate. Consequently, a user of a CDA does not have to trust the CDA but its checker algorithm. Usually, a checker is simpler and its verification is feasible. To sum up, the idea of a CDA is to adapt the underlying algorithm of a program at design-time such that it verifies its own output at runtime. While certifying sequential algorithms are well-established, there are open questions on how to apply certification to distributed algorithms. In this paper, we discuss distributed checking of a distributed witness; one challenge is that all parts of a distributed witness have to be consistent with each other. Furthermore, we present a method for formal instance verification (i.e. obtaining a machine-checked proof that a particular input-output pair is correct), and implement the method in a framework for the theorem prover Coq.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01824815/document
%2 https://inria.hal.science/hal-01824815/file/469043_1_En_9_Chapter.pdf
%L hal-01824815
%U https://inria.hal.science/hal-01824815
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-10854