Issue No. 01 - January (1998 vol. 24)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.663997
<p><b>Abstract</b>—This 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.</p>
Formal verification, protocol verification, communication protocol, theorem prover methodology, Larch prover, UNITY, computer-checked proof.
Boutheina Chetali, "Formal Verification of Concurrent Programs Using the Larch Prover", IEEE Transactions on Software Engineering, vol. 24, no. , pp. 46-62, January 1998, doi:10.1109/32.663997