Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

IPPS

2002

IEEE

2002

IEEE

We present a formalization of a proof of self-stabilization in the Coq proof assistant. Coq is a program allowing to deﬁne mathematical objects and properties, and to make proofs on them in a certiﬁed way. We use it to formalize a generic proof of stabilization for algorithms running on a linear net or a ring [1]. In this method net conﬁgurations are considered as words and the algorithm as a rewriting system on words.

Related Content

Added |
15 Jul 2010 |

Updated |
15 Jul 2010 |

Type |
Conference |

Year |
2002 |

Where |
IPPS |

Authors |
Pierre Courtieu |

Comments (0)