Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2000: Static Analysis pp 22–37Cite as

Model Checking as Constraint Solving

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1824))

Abstract

We show how model checking procedures for different kinds of infinite-state systems can be formalized as a generic constraint-solving procedure, viz. the saturation under a parametric set of inference rules. The procedures can be classified by the solved form they are to compute. This solved form is a recursive (automaton-like) definition of the set of states satisfying the given temporal property in the case of systems over stacks or other symbolic data.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bernholtz, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 142–155. Springer, Heidelberg (1994)

    Google Scholar 

  2. Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, University of Liège (May 1998)

    Google Scholar 

  3. Boigelot, B., Godefroid, P.: Symbolic verification of communications protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)

    Google Scholar 

  4. Boigelot, B., Wolper, P.: Symbolic Verification with Periodic Sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 55–67. Springer, Heidelberg (1994)

    Google Scholar 

  5. Boigelot, B., Wolper, P.: Verifying Systems with Infinite but Regular State Space. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 88–97. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  6. Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)

    Google Scholar 

  7. Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configuarations. Theoretical Computer Science 221, 211–250 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  8. Bultan, T., Gerber, R., Pugh, W.: Symbolic Model Checking of Infinitestate Systems using Presburger Arithmetics. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 400–411. Springer, Heidelberg (1997)

    Google Scholar 

  9. Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, S.S.J., Ponse, A. (eds.) Handbook of Process Algebra, Elsevier Science Publisher B.V, Amsterdam (1999) (to appear)

    Google Scholar 

  10. Burkart, O., Steffen, B.: Composition, decomposition and model checking optimal of pushdown processes. Nordic Journal of Computing 2(2), 89–125 (1995)

    MATH  MathSciNet  Google Scholar 

  11. Burkart, O., Steffen, B.: Model–checking the full modal mu–calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 419–429. Springer, Heidelberg (1997)

    Google Scholar 

  12. Chan, W., Anderson, R., Beame, P., Notkin, D.: Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-linear Constraints. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 316–327. Springer, Heidelberg (1997)

    Google Scholar 

  13. Charatonik, W., McAllester, D., Niwinski, D., Podelski, A., Walukiewicz, I.: The Horn mu-calculus. In: Pratt, V. (ed.) Proceedings of LICS 1998: Logic in Computer Science, pp. 58–69. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  14. Charatonik, W., Mukhopadhyay, S., Podelski, A.: The Sμ-calculus. Submitted to this conference

    Google Scholar 

  15. Charatonik, W., Podelski, A.: Set-based analysis of reactive infinite-state systems. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 358–375. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  16. Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: Reps, T. (ed.) Proceedings of POPL 2000: Principles of Programming Languages, January 2000, pp. 1–11. IEEE, ACM Press (2000)

    Google Scholar 

  18. Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electronic Notes in Theoretical Computer Science 9, 13 Pages (1997), www.elsevier.nl/locate/entcs

  19. Fribourg, L., Richardson, J.: Symbolic Verification with Gap-order Constraints. Technical Report LIENS-93-3, Laboratoire d’Informatique, Ecole Normale Superieure, Paris (1996)

    Google Scholar 

  20. Graf, S., Saidi, H.: Verifying invariants using theorem proving. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 196–207. Springer, Heidelberg (1996)

    Google Scholar 

  21. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: a Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997)

    Google Scholar 

  22. Larsen, K.G., Pettersson, P., Yi, W.: Compositional and symbolic model checking of real-time systems. In: Proceedings of the 16th Annual Real-time Systems Symposium, pp. 76–87. IEEE Computer Society Press, Los Alamitos (1995)

    Chapter  Google Scholar 

  23. McAllester, D.: On the complexity analysis of static analyses. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 312–329. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  24. Mukhopadhyay, S., Podelski, A.: Model checking in Uppaal and query evaluation (in preparation)

    Google Scholar 

  25. Ramakrishnan, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient Model Checking using Tabled Resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)

    Google Scholar 

  26. Shiple, T.R., Kukula, J.H., Ranjan, R.K.: A Comparison of Presburger Engines for EFSM Reachability. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 280–292. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  27. Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 208–219. Springer, Heidelberg (1996)

    Google Scholar 

  28. Walukiewicz, I.: Pushdown processes: Games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 62–74. Springer, Heidelberg (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Im Stadtwald, 66123, Saarbrücken, Germany

    Andreas Podelski

Authors
  1. Andreas Podelski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of California, Los Angeles, USA

    Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Podelski, A. (2000). Model Checking as Constraint Solving. In: Palsberg, J. (eds) Static Analysis. SAS 2000. Lecture Notes in Computer Science, vol 1824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45099-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45099-3_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67668-3

  • Online ISBN: 978-3-540-45099-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation