The paper describes the use of the Larch prover to verify concurrent programs. The chosen specification environment is UNITY, whose proposed model can be fruitfully applied to a wide variety of problems and modified or extended for special purposes. Moreover, UNITY provides a high level of abstraction to express solutions to parallel programming problems. We investigate how the UNITY methodology can be mechanized within a general purpose first order logic theorem prover like LP, and how we can use the theorem proving methodology to prove safety and liveness properties. Then we describe the formalization and the verification of a communication protocol over faulty channels, using the Larch prover LP. We present the full computer checked proof, and we show that a theorem prover can be used to detect flaws in a system specification.
展开▼
