@inproceedings{5104809773fe4b858f9b94ff1cdadb01,
title = "Verifying self-stabilizing population protocols with Coq",
abstract = "Population protocols are an elegant model recently introduced for distributed algorithms running in large and unreliable networks of tiny mobile agents. Correctness proofs of such protocols involve subtle arguments on infinite sequences of events. We propose a general formalization of self-stabilizing population protocols with the Coq proof assistant. It is used in reasoning about a concrete protocol for leader election in complete graphs. The protocol is formally proved to be correct for networks of arbitrarily large size. To this end we develop an appropriate theory of infinite sequences, including results for reasoning on abstractions. In addition, we provide a constructive correctness proof for a leader election protocol in directed rings. An advantage of using a constructive setting is that we get more informative proofs on the scenarios that converge to the desired configurations.",
keywords = "Coq, Formal verification, Population protocols, Proof assistant, Self-stabilization",
author = "Yuxin Deng and Monin, \{Jean Fran{\c c}ois\}",
year = "2009",
doi = "10.1109/TASE.2009.9",
language = "英语",
isbn = "9780769537573",
series = "Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009",
publisher = "IEEE Computer Society",
pages = "201--208",
booktitle = "Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009",
address = "美国",
note = "2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009 ; Conference date: 29-07-2009 Through 31-07-2009",
}