{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:48:07Z","timestamp":1770752887249,"version":"3.50.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540212997","type":"print"},{"value":"9783540247302","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_35","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T11:00:15Z","timestamp":1280746815000},"page":"467-481","source":"Crossref","is-referenced-by-count":108,"title":["A Temporal Logic of Nested Calls and Returns"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Kousha","family":"Etessami","sequence":"additional","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-44585-4_18","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 207\u2013220. Springer, Heidelberg (2001)"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/3-540-48224-5_54","volume-title":"Automata, Languages and Programming","author":"M. Benedikt","year":"2001","unstructured":"Benedikt, M., Godefroid, P., Reps, T.: Model checking of unrestricted hierarchical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 652\u2013666. Springer, Heidelberg (2001)"},{"key":"35_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1109\/LICS.1995.523250","volume-title":"Proc., 10th Annual IEEE Symp. on Logic in Computer Science","author":"A. Bouajjani","year":"1995","unstructured":"Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: Proc., 10th Annual IEEE Symp. on Logic in Computer Science, pp. 123\u2013133. IEEE, Los Alamitos (1995)"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Applications to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, R., Poll, E.: An overview of JML tools and applications. In: Proc. 8th International Workshop on Formal Methods for Industrial Critical Systems, pp. 75\u201389 (2003)","DOI":"10.1016\/S1571-0661(04)80810-7"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"CONCUR \u201992","author":"O. Burkart","year":"1992","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 123\u2013137. Springer, Heidelberg (1992)"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/3-540-45793-3_22","volume-title":"Computer Science Logic","author":"T. Cachat","year":"2002","unstructured":"Cachat, T., Duparc, J., Thomas, W.: Solving pushdown games with a \u03a33 winning condition. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 322\u2013336. Springer, Heidelberg (2002)"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/3-540-44898-5_7","volume-title":"Static Analysis","author":"K. Chatterjee","year":"2003","unstructured":"Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T.A., Palsberg, J.: Stack size analysis for interrupt driven programs. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 109\u2013126. Springer, Heidelberg (2003)"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Chen, H., Wagner, D.: Mops: an infrastructure for examining security properties of software. In: Proceedings of ACM Conference on Computer and Communications Security, pp. 235\u2013244 (2002)","DOI":"10.1145\/586110.586142"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"35_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","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.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"issue":"2","key":"35_CR13","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.S.: Model-checking LTL with regular valuations for pushdown systems. Information and Computation\u00a0186(2), 355\u2013376 (2003)","journal-title":"Information and Computation"},{"key":"35_CR14","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"issue":"10","key":"35_CR15","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"issue":"5","key":"35_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"35_CR17","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"Jensen, T., Le Metayer, D., Thorn, T.: Verification of control flow based security properties. In: Proc. of the IEEE Symp. on Security and Privacy, pp. 89\u2013103 (1999)","DOI":"10.1109\/SECPRI.1999.766902"},{"key":"35_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-36078-6_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kupferman","year":"2002","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Pushdown Specifications. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 262\u2013277. Springer, Heidelberg (2002)"},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45657-0_31","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2002","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Model checking linear properties of prefix-recognizable systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 371\u2013385. Springer, Heidelberg (2002)"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification. In: Proc., 12th ACM POPL, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"35_CR22","volume-title":"The temporal logic of reactive and concurrent systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: Specification. Springer, Heidelberg (1991)"},{"key":"35_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201377 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Proc. ACM POPL, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24730-2_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,2]],"date-time":"2021-11-02T14:13:11Z","timestamp":1635862391000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}