Advertisement

Model Checking Procedural Programs

  • Rajeev Alur
  • Ahmed Bouajjani
  • Javier Esparza
Chapter

Abstract

We consider the model-checking problem for sequential programs with procedure calls. We first present basic algorithms for solving the reachability problem and the fair computation problem. The algorithms are based on two techniques: summarization, which computes reachability information by solving a set of fixpoint equations, and saturation, which computes the set of all reachable program states (including call stacks) using automata. Then, we study formalisms to specify requirements of programs with procedure calls. We present an extension of Linear Temporal Logic allowing propagation of information across the hierarchical structure induced by procedure calls and matching returns. Finally, we show how model checking can be extended to this class of programs and properties.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: Proc. of the Symp. on Logic in Computer Science (LICS), pp. 151–160. IEEE, Piscataway (2007) Google Scholar
  2. 2.
    Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. Trans. Program. Lang. Syst. 27(4), 786–818 (2005) CrossRefGoogle Scholar
  3. 3.
    Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: Proc. of the Symp. on Principles of Programming Languages (POPL), pp. 153–165. ACM, New York (2006) Google Scholar
  4. 4.
    Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) Proc. of the Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004) zbMATHGoogle Scholar
  5. 5.
    Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. of the Symp. on Theory of Computing (STOC), pp. 202–211. ACM, New York (2004) Google Scholar
  6. 6.
    Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 16:1–16:43 (2009) MathSciNetCrossRefGoogle Scholar
  7. 7.
    Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. Trans. Program. Lang. Syst. 23(3), 1–31 (2001) Google Scholar
  8. 8.
    Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011) CrossRefGoogle Scholar
  9. 9.
    Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) Proc. of the Intl. Symp. on Model Checking of Software (SPIN). LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000) Google Scholar
  10. 10.
    Book, R., Otto, F.: String-Rewriting Systems. Springer, Heidelberg (1993) CrossRefGoogle Scholar
  11. 11.
    Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: Proc. of the Symp. on Logic in Computer Science (LICS), pp. 123–133. IEEE, Piscataway (1995) Google Scholar
  12. 12.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997) Google Scholar
  13. 13.
    Bouajjani, A., Habermehl, P.: Constrained properties, semilinear systems, and Petri nets. In: Montanari, U., Sassone, V. (eds.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1119, pp. 481–497. Springer, Heidelberg (1996) Google Scholar
  14. 14.
    Bouajjani, A., Meyer, A.: Symbolic reachability analysis of higher-order context-free processes. In: Lodaya, K., Mahajan, M. (eds.) Proc. of the Intl. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol. 3328, pp. 135–147 (2004) Google Scholar
  15. 15.
    Büchi, J.R.: In: Siefkes, D. (ed.) Finite Automata, Their Algebras and Grammars. Springer, Heidelberg (1988) Google Scholar
  16. 16.
    Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W. (ed.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 630, pp. 123–137. Springer, Heidelberg (1992) Google Scholar
  17. 17.
    Burkart, O., Steffen, B.: Pushdown processes: parallel composition and model checking. In: Jonsson, B., Parrow, J. (eds.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 836, pp. 98–113. Springer, Heidelberg (1994) Google Scholar
  18. 18.
    Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Proc. of the Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 1256, pp. 419–429. Springer, Heidelberg (1997) CrossRefGoogle Scholar
  19. 19.
    Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theor. Comput. Sci. 221(1–2), 251–270 (1999) MathSciNetCrossRefGoogle Scholar
  20. 20.
    Cachat, T.: Symbolic strategy synthesis for games on pushdown graphs. In: Widmayer, P., Ruiz, F.T., Bueno, R.M., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) Proc. of the Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 2380, pp. 704–715. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  21. 21.
    Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106(1), 61–86 (1992) MathSciNetCrossRefGoogle Scholar
  22. 22.
    Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) zbMATHGoogle Scholar
  23. 23.
    Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T., Palsberg, J.: Stack size analysis for interrupt driven programs. Inf. Comput. 194(2), 144–174 (2004) MathSciNetCrossRefGoogle Scholar
  24. 24.
    Chaudhuri, S., Alur, R.: Instrumenting C programs with nested word monitors. In: Bosnacki, D., Edelkamp, S. (eds.) Proc. of the Intl. Symp. on Model Checking of Software (SPIN). LNCS, vol. 4595. Springer, Heidelberg (2007) Google Scholar
  25. 25.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP WG2.2 Conference on Formal Description of Programming Concepts, pp. 237–277. North-Holland, Amsterdam (1978) zbMATHGoogle Scholar
  26. 26.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) Proc. of Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  27. 27.
    Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355–376 (2003) MathSciNetCrossRefGoogle Scholar
  28. 28.
    Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) Proc. of Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  29. 29.
    Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9, 27–37 (1997) CrossRefGoogle Scholar
  30. 30.
    Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: Nicola, R.D. (ed.) Proc. of the European Symp. on Programming (ESOP). LNCS, vol. 4421, pp. 253–267. Springer, Heidelberg (2007) Google Scholar
  31. 31.
    Hague, M., Ong, C.H.L.: Symbolic backwards-reachability analysis for higher-order pushdown systems. In: Seidl, H. (ed.) Proc. of the Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol. 4423, pp. 213–227. Springer, Heidelberg (2007) Google Scholar
  32. 32.
    Hague, M., Ong, C.H.L.: Winning regions of pushdown parity games: a saturation method. In: Bravetti, M., Zavattaro, G. (eds.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 5710, pp. 384–398. Springer, Heidelberg (2009) Google Scholar
  33. 33.
    Hague, M., Ong, C.H.L.: A saturation method for the modal \(\mu\)-calculus over pushdown systems. Inf. Comput. 209(5), 799–821 (2011) MathSciNetCrossRefGoogle Scholar
  34. 34.
    Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) Proc. of the Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  35. 35.
    Jensen, T., Metayer, D.L., Thorn, T.: Verification of control flow based security properties. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 89–103 (1999) Google Scholar
  36. 36.
    Jha, S., Schwoon, S., Wang, H., Reps, T.W.: Weighted pushdown systems and trust-management systems. In: Hermanns, H., Palsberg, J. (eds.) Proc. of the Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3920, pp. 1–26. Springer, Heidelberg (2006) Google Scholar
  37. 37.
    Kidd, N., Lal, A., Reps, T.: WALi: the weighted automata library. See http://www.cs.wisc.edu/wpis/wpds/
  38. 38.
    Kupferman, O.: Automata theory and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  39. 39.
    Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51–75 (1985) MathSciNetCrossRefGoogle Scholar
  40. 40.
    Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. of the Symp. on Principles of Programming Languages (POPL), pp. 330–341. ACM, New York (2004) Google Scholar
  41. 41.
    Parikh, R.: On context-free languages. J. ACM 13(4), 570–581 (1966) CrossRefGoogle Scholar
  42. 42.
    Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  43. 43.
    Piterman, N., Vardi, M.Y.: Global model-checking of infinite-state systems. In: Alur, R., Peled, D. (eds.) Proc. of the Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 3114, pp. 387–400. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  44. 44.
    Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proc. of the Symp. on Principle of Programming Languages (POPL), pp. 49–61. ACM, New York (1995) Google Scholar
  45. 45.
    Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1–2), 206–263 (2005). Special Issue on the Static Analysis Symposium 2003 MathSciNetCrossRefGoogle Scholar
  46. 46.
    Sagiv, S., Reps, T.W., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167(1&2), 131–170 (1996) MathSciNetCrossRefGoogle Scholar
  47. 47.
    Schwoon, S.: Model-checking pushdown systems. Ph.D. thesis, TU München (2002) Google Scholar
  48. 48.
    Seth, A.: An alternative construction in symbolic reachability analysis of second order pushdown systems. Int. J. Found. Comput. Sci. 19(4), 983–998 (2008) MathSciNetCrossRefGoogle Scholar
  49. 49.
    Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189–233. Prentice-Hall, New York (1981) Google Scholar
  50. 50.
    Song, F., Touili, T.: Efficient CTL model checking for pushdown systems. In: Katoen, J.P., König, B. (eds.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 6901, pp. 434–449. Springer, Heidelberg (2011) Google Scholar
  51. 51.
    Steffen, B., Claßen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995) Google Scholar
  52. 52.
    Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: a Java bytecode checker based on Moped. In: Halbwachs, N., Zuck, L.D. (eds.) Proc. of the Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 541–545. Springer, Heidelberg (2005) zbMATHGoogle Scholar
  53. 53.
    Walukiewicz, I.: Pushdown processes: games and model checking. In: Alur, R., Henzinger, T.A. (eds.) Proc. of the Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1102, pp. 62–74. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  54. 54.
    Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Proc. of the Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol. 1974, pp. 127–138. Springer, Heidelberg (2000) Google Scholar
  55. 55.
    Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234–263 (2001) MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.University of PennsylvaniaPhiladelphiaUSA
  2. 2.Institut Universitaire de France, Paris Diderot University (Paris 7)ParisFrance
  3. 3.Technical University of MunichMunichGermany

Personalised recommendations