A formal proof of a protocol for communications over faulty channels using the Larch Prover

Abstract : This paper describes, by means of an example, how one may mechanically verify concurrent programs on the automated theorem prover {\sc Lp}. It presents a fully computer checked proof of a protocol for communications over faulty channels. The chosen specification environment is {\sc Unity}, since the proposed model can be fruitfully applied to a wide variety of problems and modified or extended for special purposes. It provides a higher level of abstraction to express solutions to parallel programming problems. We investigate how the {\sc Unity} methodology can be mechanized in {\sc Lp}, and how we can use the theorem proving methodology to prove safety and liveness.
Type de document :
Rapport
[Research Report] RR-2476, INRIA. 1995
Liste complète des métadonnées

https://hal.inria.fr/inria-00074198
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:44:09
Dernière modification le : samedi 17 septembre 2016 - 01:06:51
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:06:32

Fichiers

Identifiants

  • HAL Id : inria-00074198, version 1

Collections

Citation

Boutheina Chetali. A formal proof of a protocol for communications over faulty channels using the Larch Prover. [Research Report] RR-2476, INRIA. 1995. 〈inria-00074198〉

Partager

Métriques

Consultations de la notice

151

Téléchargements de fichiers

95