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.
Access provided by CONRICYT-eBooks. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
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)
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)
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)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. of the Symp. on Theory of Computing (STOC), pp. 202–211. ACM, New York (2004)
Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 16:1–16:43 (2009)
Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. Trans. Program. Lang. Syst. 23(3), 1–31 (2001)
Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)
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)
Book, R., Otto, F.: String-Rewriting Systems. Springer, Heidelberg (1993)
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)
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)
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)
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)
Büchi, J.R.: In: Siefkes, D. (ed.) Finite Automata, Their Algebras and Grammars. Springer, Heidelberg (1988)
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)
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)
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)
Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theor. Comput. Sci. 221(1–2), 251–270 (1999)
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)
Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106(1), 61–86 (1992)
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)
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)
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)
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)
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)
Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355–376 (2003)
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)
Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9, 27–37 (1997)
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)
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)
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)
Hague, M., Ong, C.H.L.: A saturation method for the modal \(\mu\)-calculus over pushdown systems. Inf. Comput. 209(5), 799–821 (2011)
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)
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)
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)
Kidd, N., Lal, A., Reps, T.: WALi: the weighted automata library. See http://www.cs.wisc.edu/wpis/wpds/
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)
Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51–75 (1985)
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)
Parikh, R.: On context-free languages. J. ACM 13(4), 570–581 (1966)
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)
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)
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)
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
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)
Schwoon, S.: Model-checking pushdown systems. Ph.D. thesis, TU München (2002)
Seth, A.: An alternative construction in symbolic reachability analysis of second order pushdown systems. Int. J. Found. Comput. Sci. 19(4), 983–998 (2008)
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)
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)
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)
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)
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)
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)
Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234–263 (2001)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Alur, R., Bouajjani, A., Esparza, J. (2018). Model Checking Procedural Programs. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-10575-8_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10574-1
Online ISBN: 978-3-319-10575-8
eBook Packages: Computer ScienceComputer Science (R0)