{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:17:11Z","timestamp":1725981431194},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319941103"},{"type":"electronic","value":"9783319941110"}],"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-94111-0_9","type":"book-chapter","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:07:44Z","timestamp":1529075264000},"page":"153-170","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Branching Time Variant of CaRet"],"prefix":"10.1007","author":[{"given":"Jens Oliver","family":"Gutsfeld","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benedikt","family":"Nordhoff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,16]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Arenas, M., Barcel\u00f3, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. Log. Methods Comput. Sci. 4(4) (2008). https:\/\/lmcs.episciences.org\/782","DOI":"10.2168\/LMCS-4(4:11)2008"},{"issue":"4","key":"9_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. ACM Trans. Program. Lang. Syst. 27(4), 786\u2013818 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"9_CR3","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1145\/1111320.1111051","volume":"41","author":"Rajeev Alur","year":"2006","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: POPL 2006, pp. 153\u2013165 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/11817963_31","volume-title":"Computer Aided Verification","author":"R Alur","year":"2006","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: Languages of nested trees. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 329\u2013342. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_31"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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.) TACAS 2004. LNCS, vol. 2988, pp. 467\u2013481. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_35"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC 2004, pp. 202\u2013211 (2004)","DOI":"10.1145\/1007352.1007390"},{"issue":"3","key":"9_CR7","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"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63141-0_10"},{"issue":"1\u20132","key":"9_CR9","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1016\/j.tcs.2007.03.049","volume":"379","author":"L Bozzelli","year":"2007","unstructured":"Bozzelli, L.: Complexity results on branching-time pushdown model checking. Theor. Comput. Sci. 379(1\u20132), 286\u2013297 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/j.entcs.2009.02.045","volume":"231","author":"L Bozzelli","year":"2009","unstructured":"Bozzelli, L.: CaRet with forgettable past. Electr. Notes Theor. Comput. Sci. 231, 343\u2013361 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s10817-017-9410-z","volume":"60","author":"L Bozzelli","year":"2018","unstructured":"Bozzelli, L., S\u00e1nchez, C.: Visibly linear temporal logic. J. Autom. Reason. 60(2), 177\u2013220 (2018)","journal-title":"J. Autom. Reason."},{"key":"9_CR12","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. 630, pp. 123\u2013137. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0084787"},{"issue":"1\u20132","key":"9_CR13","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":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/3-540-45465-9_60","volume-title":"Automata, Languages and Programming","author":"T Cachat","year":"2002","unstructured":"Cachat, T.: Symbolic strategy synthesis for games on pushdown graphs. In: Widmayer, P., Eidenbenz, S., Triguero, F., Morales, R., Conejo, R., Hennessy, M. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 704\u2013715. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45465-9_60"},{"key":"9_CR15","unstructured":"Cachat, T.: Games on pushdown graphs and extensions. Ph.D. thesis, RWTH Aachen University, Germany (2003)"},{"key":"9_CR16","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. 1855, pp. 232\u2013247. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_20"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FoSSaCS 1999. LNCS, vol. 1578, pp. 14\u201330. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49019-1_2"},{"issue":"2","key":"9_CR18","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":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","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.) CAV 2001. LNCS, vol. 2102, pp. 324\u2013336. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_30"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-04081-8_26","volume-title":"CONCUR 2009 - Concurrency Theory","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.) CONCUR 2009. LNCS, vol. 5710, pp. 384\u2013398. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_26"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-33475-7_16","volume-title":"Theoretical Computer Science","author":"S Torre La","year":"2012","unstructured":"La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 225\u2013239. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33475-7_16"},{"key":"9_CR22","unstructured":"Nguyen, H., Touili, T.: CARET analysis of multithreaded programs. CoRR abs\/1709.09006 (2017)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Nguyen, H., Touili, T.: CARET model checking for malware detection. In: SPIN Symposium 2017, pp. 152\u2013161 (2017)","DOI":"10.1145\/3092282.3092301"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Nguyen, H., Touili, T.: CARET model checking for pushdown systems. In: SAC 2017, pp. 1393\u20131400 (2017)","DOI":"10.1145\/3019612.3019829"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-89247-2_4","volume-title":"Runtime Verification","author":"G Ro\u015fu","year":"2008","unstructured":"Ro\u015fu, G., Chen, F., Ball, T.: Synthesizing monitors for safety properties: this time with calls and returns. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 51\u201368. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89247-2_4"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: POPL 1998, pp. 38\u201348 (1998)","DOI":"10.1145\/268946.268950"},{"key":"9_CR27","unstructured":"Schwoon, S.: Model checking pushdown systems. Ph.D. thesis, Technical University Munich, Germany (2002)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: PuMoC: a CTL model-checker for sequential programs. In: ASE 2012, pp. 346\u2013349 (2012)","DOI":"10.1145\/2351676.2351743"},{"key":"9_CR29","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.tcs.2014.07.001","volume":"549","author":"F Song","year":"2014","unstructured":"Song, F., Touili, T.: Efficient CTL model-checking for pushdown systems. Theor. Comput. Sci. 549, 127\u2013145 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346\u2013364. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54415-1_54"},{"issue":"2","key":"9_CR31","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."},{"key":"9_CR32","unstructured":"Weinert, A., Zimmermann, M.: Visibly linear dynamic logic. In: FSTTCS 2016, 13\u201315 December 2016, pp. 28:1\u201328:14 (2016)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94111-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:24:13Z","timestamp":1571480653000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94111-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319941103","9783319941110"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94111-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}