Lawrence C. Paulson and Michael J. C. Gordon (with thanks to Sara Kalvala)

Computer Laboratory, University of Cambridge

Research associates: Chris Owens (to 28/2/98); Giampaolo Bella

Funded by the EPSRC (1 Nov 1995 to 31 Oct 1998).

Grant reference GR/K57381/01. Value £172,816

Automated temporal reasoning has many applications to industrial problems. Examples range from the use of model checkers for verifying the consistency of cache protocols to proof tools for reasoning about telecommunication software. This project has developed a theorem proving environment that supports temporal reasoning in the UNITY formalism. We have used Isabelle as our implementation platform and have embedded the semantics of UNITY within higher-order logic. UNITY actions are modelled as relations on states. Safety and liveness reasoning is supported, as is program composition (also called program union). Thus, the full meta-theory of UNITY has been developed formally. Numerous examples have been undertaken, including the well-known Lift example. Safety proofs are often automatic.

Lawrence C. Paulson • Computer Laboratory • University of Cambridge