# Formal Verification of Concurrent Program using the Larch Prover

**Boutheina Chetali**

**In TACAS, pages
174--186**

### Abstract:

*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.*

** Comments**

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

Available as * PostScript*,
* DVI*.

BRICS WWW home page