Symbolic model checking of infinite state systems using presburger arithmetic

  • Tevfik Bultan
  • Richard Gerber
  • William Pugh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


We present a new symbolic model checker which conservatively evaluates safety and liveness properties on infinite-state programs. We use Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations. All fixpoint calculations are executed symbolically, and their convergence is guaranteed by using approximation techniques. We demonstrate the promise of this technology on some well-known infinite-state concurrency problems.


Model Checker Transition Relation Critical Section Mutual Exclusion Liveness Property 
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. 1.
    R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3–34, 1995.Google Scholar
  2. 2.
    G. R. Andrews. Concurrent Programming, Principles and Practice. The Benjamin/Cummings Publishing Company, 1991.Google Scholar
  3. 3.
    A. Arnold. Finite Transition Systems: Semantics of Communicating Systems. Prentice Hall, 1994.Google Scholar
  4. 4.
    R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.Google Scholar
  5. 5.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. H. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th Annual IEEE Symp. on Logic in Computer Science, pages 428–439, 1990.Google Scholar
  6. 6.
    T. Bultan, J. Fischer, and R. Gerber. Compositional verification by model checking for counter-examples. In Proc. 1996 Int. Symp. on Software Testing and Analysis, pages 224–238, 1996.Google Scholar
  7. 7.
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.Google Scholar
  8. 8.
    E. M. Clarke, O. Grumberg, D. E. Long Model checking and abstraction. In Proc. 18th Annual ACM Symp. on Principles of Programming Languages, pages 343–354, 1992.Google Scholar
  9. 9.
    E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proc. 4th Annual IEEE Symp. on Logic in Computer Science, pages 464–475, 1989.Google Scholar
  10. 10.
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th Annual ACM Symp. on Principles of Programming Languages, pages 238–252, 1977.Google Scholar
  11. 11.
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th Annual ACM Symp. on Principles of Programming Languages, pages 84–97, 1978.Google Scholar
  12. 12.
    J. Dingel, and T. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In Proc. 7th Int. Conference on Computer Aided Verification, LNCS 939, pages 54–69, 1995.Google Scholar
  13. 13.
    M. J. Fischer and M. O. Rabin. Super-Exponential Complexity of Presburger Arithmetic. SIAM-AMS Proc., Volume 7, pages 27–41, 1974.Google Scholar
  14. 14.
    P. Godefroid. Partial-order methods for the verification of concurrent systems: An approach to the state-explosion problem. Ph.D. Thesis, Universite De Liege, 1994.Google Scholar
  15. 15.
    W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman and D. Wonnacott. The Omega Library (version 1.00) interface guide. Available at <>.Google Scholar
  16. 16.
    W. Kelly, W. Pugh, E. Rosser and T. Shpeisman. Transitive closure of infinite graphs and its applications. Technical Report CS-TR-3457, UMIACS-TR-95-48, Department of Computer Science, University of Maryland, 1994.Google Scholar
  17. 17.
    W. Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:102–104, 1992.Google Scholar
  18. 18.
    A. Udaya Shankar. An introduction to assertional reasoning for concurrent systems. ACM Computing Surveys, 25(3):225–262, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Tevfik Bultan
    • 1
  • Richard Gerber
    • 1
  • William Pugh
    • 1
  1. 1.Department of Computer ScienceUniversity of MarylandCollege ParkUSA

Personalised recommendations