Symbolic model checking with rich assertional languages

  • Y. Resten
  • O. Maler
  • M. Marcus
  • A. Pnueli
  • E. Shahar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


The paper shows that, by an appropriate choice of a rich assertional language, it is possible to extend the utility of symbolic model checking beyond the realm of BDD-represented finite-state systems into the domain of infinite-state systems, leading to a powerful technique for uniform verification of unbounded (parameterized) process networks.

The main contributions of the paper are a formulation of a general framework for symbolic model checking of infinite-state systems, a demonstration that many individual examples of uniformly verified parameterized designs that appear in the literature are special cases of our general approach, verifying the correctness of the Futurebus+ design for all singlebus configurations, extending the technique to tree architectures, and establishing that the presented method is a precise dual to the top-down invariant generation method used in deductive verification.


Regular Expression Critical Section Regular Language Tree Automaton Tree 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.


  1. [AK86]
    K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.Google Scholar
  2. [BBM95]
    N. Bjørner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. In LNCS 976, 1995.Google Scholar
  3. [BO93]
    R.V. Book and F. Otto. String-Rewriting Systems, Springer, 1993.Google Scholar
  4. [BM96]
    A. Bouajjani and O. Maler, Reachability Analysis of Push-down Automata. Workshop on Infinite-state Systems, Pisa, 1996.Google Scholar
  5. [BCG86]
    M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. In PODC'86.Google Scholar
  6. [BCM+92]
    J.R. Burch, E.M. Clarke, et al. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.Google Scholar
  7. [BK95]
    D.A. Basin and N. Klarlund. Hardware verification using 2nd-order logic. In P. Wolper, editor, CAV'95, LNCS 939, 1995.Google Scholar
  8. [BLS96]
    S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. CAV'96, 1996.Google Scholar
  9. [Bry86]
    R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(12):1035–1044, 1986.Google Scholar
  10. [CE81]
    E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. Logics of Programs, LNCS 131, 1981.Google Scholar
  11. [CES86]
    E.M. Clarke, et al. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Sys., 1986.Google Scholar
  12. [CGH+93]
    E.M. Clarke, O. Grumberg, et al. Verification of the futurebus+ cache coherence protocol. Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. 1993.Google Scholar
  13. [CGJ95]
    E.M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In CONCUR'95, 1995.Google Scholar
  14. [D70]
    J. Doner. Tree Acceptors and some of their applications, JCSS 4, 1970.Google Scholar
  15. [EN95]
    E. A. Emerson, K. S. Namjoshi. Reasoning about rings. POPL'95, 1995.Google Scholar
  16. [EN96]
    E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, CAV'96, 1996.Google Scholar
  17. [GS70]
    F. Gecseg and M. Steinby. Tree Automata Akademiai Kiado, 1984.Google Scholar
  18. [HLR92]
    N. Halbwachs, F. Lagnier, et al. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6/7), 1992.Google Scholar
  19. [HJJ+96]
    J.G. Henriksen, J. Jensen, et al. Mona: Monadic second-order logic in practice. In TACAS '95, LNCS 1019, 1996.Google Scholar
  20. [ID96]
    C.N. Ip and D. Dill. Verifying systems with replicated components in Munϕ. In R. Alur and T. Henzinger, editors, CAV'96, 1996.Google Scholar
  21. [KG96]
    O. Kupferman and O. Grumberg. Branching Time Temporal Logic and Amorphous Tree Automata. Information and Computation 125, 1996.Google Scholar
  22. [KM89]
    R.P. Kurshan and K. McMillan. A structural induction theorem for processes. In P. Rudnicki, editor, PODC'89, Edmonton, AB, Canada, 1989.Google Scholar
  23. [LHR97]
    D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL'97, Paris, 1997.Google Scholar
  24. [MAB+94]
    Z. Manna, A. Anuchitanukul, et al. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Stanford University, 1994.Google Scholar
  25. [McM93]
    K.L McMillan. Symbolic Model Checking. 1993.Google Scholar
  26. [MP95]
    Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.Google Scholar
  27. [PS96]
    A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, CAV'96, 1996.Google Scholar
  28. [QS82]
    J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. International Symposium on Programming,LNCS 137, 1982.Google Scholar
  29. [SG89]
    Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In LNCS 407, 1989.Google Scholar
  30. [SG92]
    A.P. Sistla and S.M. German. Reasoning about systems with many processes. J. ACM, 39:675–735, 1992.Google Scholar
  31. [SOR93]
    N. Shankar, S. Owre, and J.M. Rushby. The PVS proof checker: A reference manual (draft). Technical report, SRI International, Menlo Park, CA, 1993.Google Scholar
  32. [TW68]
    J.W. Thatcher, J.B. Wright. Generalized finite automata with application to a decision procedure in second order logic. Math. Sys. Theory 2, 1968.Google Scholar
  33. [WL89]
    P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In LNCS 407, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Y. Resten
    • 1
  • O. Maler
    • 2
  • M. Marcus
    • 3
  • A. Pnueli
    • 3
  • E. Shahar
    • 3
  1. 1.Future Cad TechnologyIntelIsrael
  2. 2.VerimagCentre EquationGièresFrance
  3. 3.Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations