Implementing a model checker for LEGO

  • Shenwei Yu
  • Zhaohui Luo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


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.


Model Checker Mutual Exclusion Label Transition System Prototype Verification System Imperative Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    L. Augustsson, Th. Coquand, and B. Nordström. A short description of another logical framework. In G. Huet and G. Plotkin, editors, Preliminary Proc. of Logical Frameworks, 1990.Google Scholar
  2. 2.
    Julian Bradfield and Colin Stirling. Local model checking for inifinite state spaces. Theoretical Computer Science, 96:157–174, 1992.CrossRefGoogle Scholar
  3. 3.
    Glenn Bruns. Algebraic Abstraction with Process Preorders. in preparation, 1995.Google Scholar
  4. 4.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.Google Scholar
  5. 5.
    E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In D.L. Dill, editor, Proc. 6th Conference on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 415–427, Stanford, CA, June 1994. Springer Verlag.Google Scholar
  6. 6.
    R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Pretice-Hall, 1986.Google Scholar
  7. 7.
    Nicolaas G. de Bruijn. Lamda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math., 34:381–392, 1972.Google Scholar
  8. 8.
    G. Dowek et al. The Coq Proof Assistent: User's Guide (version 5.6). INRIA-Rocquencourt and CNRS-ENS Lyon, 1991.Google Scholar
  9. 9.
    E.A. Emerson and C.L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the 10th Symposium on Principles of Programming Languages, pages 84–96, New Orleans, LA, January 1985. Association for Computing Machinery.Google Scholar
  10. 10.
    Urban Engberg, Peter Gronning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In G.V. Bochmann and D.K. Probst, editors, Computer-Aided Verification 92, volume 663 of Lecture Notes in Computer Science, pages 44–55. Springer-Verlag, 1992.Google Scholar
  11. 11.
    Jeffrey J. Joyce and Carl-Johan H. Seger. Linking Bdd-based symbolic evaluation to interactive theorem proving. In Proceedings of the 30th Design Automation Conference. Association for Computing Machinery, 1993.Google Scholar
  12. 12.
    R. Kurshan and L. Lamport. Verification of a multiplier: 64 bits and beyond. In Costas Courcoubetis, editor, Computer-Aided Verification 93, volume 697 of Lecture Notes in Computer Science, pages 166–179, Elounda, Greece, June/July 1993. Springer Verlag.Google Scholar
  13. 13.
    Robert P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey, 1994.Google Scholar
  14. 14.
    R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In 8th ACM Symposium on Principles of Distributed Computing, pages 239–248, Edmonton, Albera, Canada, August 1989.Google Scholar
  15. 15.
    Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, 1994.Google Scholar
  16. 16.
    Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992.Google Scholar
  17. 17.
    L. Magnusson. The new implementation of ALF. In Informal Proceedings of Workshop on Logical Frameworks, Bastad, 1992.Google Scholar
  18. 18.
    Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993.Google Scholar
  19. 19.
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  20. 20.
    Olaf Milller and Tobias Nipkow. Combining Model Checking and Deduction for I/O-Automata. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1019 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, 1995.Google Scholar
  21. 21.
    S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automted Deduction(CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag.Google Scholar
  22. 22.
    Randy Pollack. Incremental Changes in LEGO: 1994, May 1994. Available by ftp with LEGO distribution.Google Scholar
  23. 23.
    Robert Pollack. A Verified Typechecker. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, Edinburgh, 1995. Springer-Verlag.Google Scholar
  24. 24.
    S. Rajan, N. Shankar, and M. K. Srivas. An Integration of Model Checking with Automated Proof checking. In Computer Aided Verification, Proc. 7th Int. Conference, volume 939 of Lecture Notes in Computer Science, pages 84–97, Liège, Belgium, July 1995. Springer-Verlag.Google Scholar
  25. 25.
    Glynn Winskel. A note on model checking the modal v-calculus. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Proceedings of ICALP, volume 372 of Lecture Notes in Computer Science, pages 761–772. Springer-Verlag, 1989.Google Scholar
  26. 26.
    P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In J. Sifakis, editor, International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 68–80, Grenoble, France, June 1989. Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Shenwei Yu
    • 1
  • Zhaohui Luo
    • 1
  1. 1.Department of Computer ScienceUniversity of DurhamDurhamUK

Personalised recommendations