Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074198
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:44:09 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Monday, April 5, 2010 - 12:06:32 AM

Identifiers

  • 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⟩

Share

Metrics

Record views

196

Files downloads

166