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.