%0 Conference Proceedings
%T Squeezing Streams and Composition of Self-stabilizing Algorithms
%+ VERIMAG (VERIMAG - IMAG)
%A Altisen, Karine
%A Corbineau, Pierre
%A Devismes, Stéphane
%Z Part 1: Full 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 21-38
%8 2019-06-17
%D 2019
%R 10.1007/978-3-030-21759-4_2
%K Coq proof assistant
%K Streams
%K Coinduction
%K Composition
%K Distributed algorithm
%K Self-stabilization
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Composition is a fundamental tool when dealing with complex systems. We study the hierarchical collateral composition which is used to combine self-stabilizing distributed algorithms. The PADEC library is a framework developed with the Coq proof assistant and dedicated to the certification of self-stabilizing algorithms. We enrich PADEC with the composition operator and a sufficient condition to show its correctness. The formal proof of the condition leads us to develop new tools and methods on potentially infinite streams, these latter ones being used to model the algorithms’ executions. The cornerstone has been the definition of the function which removes duplicates from streams.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02313746/document
%2 https://inria.hal.science/hal-02313746/file/478668_1_En_2_Chapter.pdf
%L hal-02313746
%U https://inria.hal.science/hal-02313746
%~ UGA
%~ IMAG
%~ CNRS
%~ INPG
%~ VERIMAG
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-11535
%~ UGA-COMUE
%~ ANR