Formal Verification of Concurrent Program using the Larch Prover

Boutheina Chetali

In TACAS, pages 174--186


This paper describes, by means of an example, how one may mechanically verify concurrent programs on the theorem prover LP. The chosen specification environment is UNITY, a subset of ordinary temporal logic for specifying and verifying programs. We present the proof of a lift-control program, we explain how we can use the theorem proving methodology to prove safety and liveness, and to get semi-automated proofs.

CRIN-CNRS and INRIA-Lorraine, Nancy, France.

Available as PostScript, DVI.

[BRICS symbol] BRICS WWW home page