The directory presents verification examples involving program composition. They are mostly taken from the works of Chandy, Charpentier and Chandy.
Counter.thy
)
and priority system (Priority.thy
)
Alloc.thy
)
Client.thy
)
AllocImpl.thy
)
Handshake.thy
)
TimerArray.thy
)
Safety proofs (invariants) are often proved automatically. Progress proofs involving ENSURES can sometimes be proved automatically. The level of automation appears to be about the same as in HOL-UNITY by Flemming Andersen et al.
lcp@cl.cam.ac.uk