%0 Conference Proceedings
%T On Certifying Distributed Algorithms: Problem of Local Correctness
%+ Humboldt-Universität zu Berlin = Humboldt University of Berlin = Université Humboldt de Berlin  (HU Berlin)
%A Völlinger, Kim
%Z Part 2: Short and “Journal First” Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Copenhagen, Denmark
%Y Jorge A. Pérez
%Y Nobuko Yoshida
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-11535
%P 281-288
%8 2019-06-17
%D 2019
%R 10.1007/978-3-030-21759-4_16
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X A certifying distributed algorithm (CDA) is a runtime verification method for distributed systems. Additionally to each output, a CDA computes a witness – a correctness argument for the particular output. If the witness is verified at runtime, the output is correct. The output is distributed over the system with each component holding its part of the distributed output.In this paper, we investigate the case where the verification at runtime fails. Assume one component computes its part of the distributed output incorrectly. As a consequence, the distributed output is incorrect and the verification fails. Some components may still hold a correct part of the output. That is why we introduce the problem of local correctness of a component: Is a component’s part of the output correct? As a case study, we investigate local correctness for a CDA computing shortest paths as used in distance-vector routing.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02313747/document
%2 https://inria.hal.science/hal-02313747/file/478668_1_En_16_Chapter.pdf
%L hal-02313747
%U https://inria.hal.science/hal-02313747
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-11535