Implementing a model checker for LEGO
Shenwei Yu and Zhaohui Luo
Interactive theorem proving provides a general approach to modelling and
verification of both hardware and software systems but requires
significant human efforts to deal with many tedious proofs. To be
effectively used in practice, we need some automatic tools such as model
checkers to deal with those tedious proofs. In this paper, we formalise
a verification system of both CCS and an imperative language in the
proof development system LEGO which can be used to verify both finite
and infinite problems. Then a model checker, LegoMC, is implemented to
generate LEGO proof terms for finite-state problems automatically.
Therefore people can use LEGO to verify a general problem with some of
its finite sub-problems verified by LegoMC. On the other hand, this
integration extends the power of model checking to verify more
complicated and infinite models as well.
Healfdene Goguen
Last modified: Mon Jul 14 16:27:28 BST 1997