{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:56:54Z","timestamp":1770753414763,"version":"3.50.0"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_17","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"541-572","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Model Checking Procedural Programs"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"17_CR1","first-page":"151","volume-title":"Proc. of the Symp. on Logic in Computer Science (LICS)","author":"R. Alur","year":"2007","unstructured":"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.\u00a0151\u2013160. IEEE, Piscataway (2007)"},{"issue":"4","key":"17_CR2","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R. Alur","year":"2005","unstructured":"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\u2013818 (2005)","journal-title":"Trans. Program. Lang. Syst."},{"key":"17_CR3","first-page":"153","volume-title":"Proc. of the Symp. on Principles of Programming Languages (POPL)","author":"R. Alur","year":"2006","unstructured":"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.\u00a0153\u2013165. ACM, New York (2006)"},{"key":"17_CR4","series-title":"LNCS","first-page":"467","volume-title":"Proc. of the Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"R. Alur","year":"2004","unstructured":"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.\u00a02988, pp.\u00a0467\u2013481. Springer, Heidelberg (2004)"},{"key":"17_CR5","first-page":"202","volume-title":"Proc. of the Symp. on Theory of Computing (STOC)","author":"R. Alur","year":"2004","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. of the Symp. on Theory of Computing (STOC), pp.\u00a0202\u2013211. ACM, New York (2004)"},{"issue":"3","key":"17_CR6","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R. Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 16:1\u201316:43 (2009)","journal-title":"J. ACM"},{"issue":"3","key":"17_CR7","first-page":"1","volume":"23","author":"R. Alur","year":"2001","unstructured":"Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. Trans. Program. Lang. Syst. 23(3), 1\u201331 (2001)","journal-title":"Trans. Program. Lang. Syst."},{"issue":"7","key":"17_CR8","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T. Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"17_CR9","series-title":"LNCS","first-page":"113","volume-title":"Proc. of the Intl. Symp. on Model Checking of Software (SPIN)","author":"T. Ball","year":"2000","unstructured":"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.\u00a01885, pp.\u00a0113\u2013130. Springer, Heidelberg (2000)"},{"key":"17_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9771-7","volume-title":"String-Rewriting Systems","author":"R. Book","year":"1993","unstructured":"Book, R., Otto, F.: String-Rewriting Systems. Springer, Heidelberg (1993)"},{"key":"17_CR11","first-page":"123","volume-title":"Proc. of the Symp. on Logic in Computer Science (LICS)","author":"A. Bouajjani","year":"1995","unstructured":"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.\u00a0123\u2013133. IEEE, Piscataway (1995)"},{"key":"17_CR12","series-title":"LNCS","first-page":"135","volume-title":"Proc. of the Intl. Conf. on Concurrency Theory (CONCUR)","author":"A. Bouajjani","year":"1997","unstructured":"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.\u00a01243, pp.\u00a0135\u2013150. Springer, Heidelberg (1997)"},{"key":"17_CR13","series-title":"LNCS","first-page":"481","volume-title":"Proc. of the Intl. Conf. on Concurrency Theory (CONCUR)","author":"A. Bouajjani","year":"1996","unstructured":"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.\u00a01119, pp.\u00a0481\u2013497. Springer, Heidelberg (1996)"},{"key":"17_CR14","series-title":"LNCS","first-page":"135","volume-title":"Proc. of the Intl. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"A. Bouajjani","year":"2004","unstructured":"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.\u00a03328, pp.\u00a0135\u2013147 (2004)"},{"key":"17_CR15","volume-title":"Finite Automata, Their Algebras and Grammars","author":"J.R. B\u00fcchi","year":"1988","unstructured":"B\u00fcchi, J.R.: In: Siefkes, D. (ed.) Finite Automata, Their Algebras and Grammars. Springer, Heidelberg (1988)"},{"key":"17_CR16","series-title":"LNCS","first-page":"123","volume-title":"Proc. of the Intl. Conf. on Concurrency Theory (CONCUR)","author":"O. Burkart","year":"1992","unstructured":"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.\u00a0630, pp.\u00a0123\u2013137. Springer, Heidelberg (1992)"},{"key":"17_CR17","series-title":"LNCS","first-page":"98","volume-title":"Proc. of the Intl. Conf. on Concurrency Theory (CONCUR)","author":"O. Burkart","year":"1994","unstructured":"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.\u00a0836, pp.\u00a098\u2013113. Springer, Heidelberg (1994)"},{"key":"17_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Proc. of the Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"O. Burkart","year":"1997","unstructured":"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.\u00a01256, pp.\u00a0419\u2013429. Springer, Heidelberg (1997)"},{"issue":"1\u20132","key":"17_CR19","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0304-3975(99)00034-1","volume":"221","author":"O. Burkart","year":"1999","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theor. Comput. Sci. 221(1\u20132), 251\u2013270 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/3-540-45465-9_60","volume-title":"Proc. of the Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"T. Cachat","year":"2002","unstructured":"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.\u00a02380, pp.\u00a0704\u2013715. Springer, Heidelberg (2002)"},{"issue":"1","key":"17_CR21","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106(1), 61\u201386 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR22","volume-title":"Handbook of Model Checking","author":"S. Chaki","year":"2018","unstructured":"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)"},{"issue":"2","key":"17_CR23","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.ic.2004.06.001","volume":"194","author":"K. Chatterjee","year":"2004","unstructured":"Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T., Palsberg, J.: Stack size analysis for interrupt driven programs. Inf. Comput. 194(2), 144\u2013174 (2004)","journal-title":"Inf. Comput."},{"key":"17_CR24","series-title":"LNCS","volume-title":"Proc. of the Intl. Symp. on Model Checking of Software (SPIN)","author":"S. Chaudhuri","year":"2007","unstructured":"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.\u00a04595. Springer, Heidelberg (2007)"},{"key":"17_CR25","first-page":"237","volume-title":"IFIP WG2.2 Conference on Formal Description of Programming Concepts","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP WG2.2 Conference on Formal Description of Programming Concepts, pp.\u00a0237\u2013277. North-Holland, Amsterdam (1978)"},{"key":"17_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Proc. of Intl. Conf. on Computer-Aided Verification (CAV)","author":"J. Esparza","year":"2000","unstructured":"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.\u00a01855, pp.\u00a0232\u2013247. Springer, Heidelberg (2000)"},{"issue":"2","key":"17_CR27","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J. Esparza","year":"2003","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355\u2013376 (2003)","journal-title":"Inf. Comput."},{"key":"17_CR28","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Proc. of Intl. Conf. on Computer-Aided Verification (CAV)","author":"J. Esparza","year":"2001","unstructured":"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.\u00a02102, pp.\u00a0324\u2013336. Springer, Heidelberg (2001)"},{"key":"17_CR29","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S1571-0661(05)80426-8","volume":"9","author":"A. Finkel","year":"1997","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9, 27\u201337 (1997)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"17_CR30","series-title":"LNCS","first-page":"253","volume-title":"Proc. of the European Symp. on Programming (ESOP)","author":"S. Gulwani","year":"2007","unstructured":"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.\u00a04421, pp.\u00a0253\u2013267. Springer, Heidelberg (2007)"},{"key":"17_CR31","series-title":"LNCS","first-page":"213","volume-title":"Proc. of the Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS)","author":"M. Hague","year":"2007","unstructured":"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.\u00a04423, pp.\u00a0213\u2013227. Springer, Heidelberg (2007)"},{"key":"17_CR32","series-title":"LNCS","first-page":"384","volume-title":"Proc. of the Intl. Conf. on Concurrency Theory (CONCUR)","author":"M. Hague","year":"2009","unstructured":"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.\u00a05710, pp.\u00a0384\u2013398. Springer, Heidelberg (2009)"},{"issue":"5","key":"17_CR33","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1016\/j.ic.2010.12.004","volume":"209","author":"M. Hague","year":"2011","unstructured":"Hague, M., Ong, C.H.L.: A saturation method for the modal \u03bc$\\mu$-calculus over pushdown systems. Inf. Comput. 209(5), 799\u2013821 (2011)","journal-title":"Inf. Comput."},{"key":"17_CR34","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Verification (CAV)","author":"T. Henzinger","year":"2002","unstructured":"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.\u00a02404, pp.\u00a0526\u2013538. Springer, Heidelberg (2002)"},{"key":"17_CR35","first-page":"89","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"T. Jensen","year":"1999","unstructured":"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.\u00a089\u2013103 (1999)"},{"key":"17_CR36","series-title":"LNCS","first-page":"1","volume-title":"Proc. of the Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Jha","year":"2006","unstructured":"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.\u00a03920, pp.\u00a01\u201326. Springer, Heidelberg (2006)"},{"key":"17_CR37","unstructured":"Kidd, N., Lal, A., Reps, T.: WALi: the weighted automata library. See http:\/\/www.cs.wisc.edu\/wpis\/wpds\/"},{"key":"17_CR38","volume-title":"Handbook of Model Checking","author":"O. Kupferman","year":"2018","unstructured":"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)"},{"key":"17_CR39","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D.E. Muller","year":"1985","unstructured":"Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51\u201375 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR40","first-page":"330","volume-title":"Proc. of the Symp. on Principles of Programming Languages (POPL)","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. of the Symp. on Principles of Programming Languages (POPL), pp.\u00a0330\u2013341. ACM, New York (2004)"},{"issue":"4","key":"17_CR41","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R. Parikh","year":"1966","unstructured":"Parikh, R.: On context-free languages. J. ACM 13(4), 570\u2013581 (1966)","journal-title":"J. ACM"},{"key":"17_CR42","volume-title":"Handbook of Model Checking","author":"N. Piterman","year":"2018","unstructured":"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)"},{"key":"17_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-27813-9_30","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Verification (CAV)","author":"N. Piterman","year":"2004","unstructured":"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.\u00a03114, pp.\u00a0387\u2013400. Springer, Heidelberg (2004)"},{"key":"17_CR44","first-page":"49","volume-title":"Proc. of the Symp. on Principle of Programming Languages (POPL)","author":"T. Reps","year":"1995","unstructured":"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.\u00a049\u201361. ACM, New York (1995)"},{"issue":"1\u20132","key":"17_CR45","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T. Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1\u20132), 206\u2013263 (2005). Special Issue on the Static Analysis Symposium 2003","journal-title":"Sci. Comput. Program."},{"issue":"1&2","key":"17_CR46","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0304-3975(96)00072-2","volume":"167","author":"S. Sagiv","year":"1996","unstructured":"Sagiv, S., Reps, T.W., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167(1&2), 131\u2013170 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR47","unstructured":"Schwoon, S.: Model-checking pushdown systems. Ph.D. thesis, TU M\u00fcnchen (2002)"},{"issue":"4","key":"17_CR48","doi-asserted-by":"publisher","first-page":"983","DOI":"10.1142\/S012905410800608X","volume":"19","author":"A. Seth","year":"2008","unstructured":"Seth, A.: An alternative construction in symbolic reachability analysis of second order pushdown systems. Int. J. Found. Comput. Sci. 19(4), 983\u2013998 (2008)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"17_CR49","first-page":"189","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp.\u00a0189\u2013233. Prentice-Hall, New York (1981)"},{"key":"17_CR50","series-title":"LNCS","first-page":"434","volume-title":"Proc. of the Intl. Conf. on Concurrency Theory (CONCUR)","author":"F. Song","year":"2011","unstructured":"Song, F., Touili, T.: Efficient CTL model checking for pushdown systems. In: Katoen, J.P., K\u00f6nig, B. (eds.) Proc. of the Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a06901, pp.\u00a0434\u2013449. Springer, Heidelberg (2011)"},{"key":"17_CR51","series-title":"LNCS","first-page":"72","volume-title":"Proc. of the Intl. Conf. on Concurrency Theory (CONCUR)","author":"B. Steffen","year":"1995","unstructured":"Steffen, B., Cla\u00dfen, 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.\u00a0962, pp.\u00a072\u201387. Springer, Heidelberg (1995)"},{"key":"17_CR52","series-title":"LNCS","first-page":"541","volume-title":"Proc. of the Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"D. Suwimonteerabuth","year":"2005","unstructured":"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.\u00a03440, pp.\u00a0541\u2013545. Springer, Heidelberg (2005)"},{"key":"17_CR53","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Proc. of the Intl. Conf. on Computer-Aided Verification (CAV)","author":"I. Walukiewicz","year":"1996","unstructured":"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.\u00a01102, pp.\u00a062\u201374. Springer, Heidelberg (1996)"},{"key":"17_CR54","series-title":"LNCS","first-page":"127","volume-title":"Proc. of the Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"I. Walukiewicz","year":"2000","unstructured":"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.\u00a01974, pp.\u00a0127\u2013138. Springer, Heidelberg (2000)"},{"issue":"2","key":"17_CR55","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I. Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234\u2013263 (2001)","journal-title":"Inf. Comput."}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:13:35Z","timestamp":1526616815000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_17","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}