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 symbol]](http://www.brics.aau.dk/BRICS/GIF/BRICS/msymbol8mm.GIF)
BRICS WWW home page