{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:02:17Z","timestamp":1743091337588,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031505201"},{"type":"electronic","value":"9783031505218"}],"license":[{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-50521-8_3","type":"book-chapter","created":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T08:03:15Z","timestamp":1703836995000},"page":"48-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Navigation Logic for\u00a0Recursive Programs with\u00a0Dynamic Thread Creation"],"prefix":"10.1007","author":[{"given":"Roman","family":"Lakenbrink","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Ohrem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Gutsfeld","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,30]]},"reference":[{"key":"3_CR1","unstructured":"Oracle Java docs: Intrinsic locks and synchronization. https:\/\/docs.oracle.com\/javase\/tutorial\/essential\/concurrency\/locksync.html"},{"key":"3_CR2","doi-asserted-by":"publisher","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:\/\/doi.org\/10.2168\/LMCS-4(4:11)2008","DOI":"10.2168\/LMCS-4(4:11)2008"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11\u201313 January 2006, pp. 153\u2013165. ACM (2006). https:\/\/doi.org\/10.1145\/1111037.1111051","DOI":"10.1145\/1111037.1111051"},{"key":"3_CR4","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":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11779148_1","volume-title":"Developments in Language Theory","author":"R Alur","year":"2006","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 1\u201313. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11779148_1"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(4:4)2011","DOI":"10.2168\/LMCS-7(4:4)2011"},{"key":"3_CR7","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"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473\u2013487. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11539452_36"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-540-74407-8_32","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"L Bozzelli","year":"2007","unstructured":"Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 476\u2013491. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_32"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-22119-4_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"L Bozzelli","year":"2011","unstructured":"Bozzelli, L., Lanotte, R.: Hybrid and first-order complete extensions of CaRet. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 58\u201372. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22119-4_7"},{"key":"3_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":"EM 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. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-030-05529-5_16","volume-title":"Networked Systems","author":"M Diaz","year":"2019","unstructured":"Diaz, M., Touili, T.: Model checking dynamic pushdown networks with locks and priorities. In: Podelski, A., Ta\u00efani, F. (eds.) NETYS 2018. LNCS, vol. 11028, pp. 240\u2013251. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-05529-5_16"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs (extended abstract). In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24\u201326 October 1988, pp. 328\u2013337. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21949","DOI":"10.1109\/SFCS.1988.21949"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-18275-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"TM Gawlitza","year":"2011","unstructured":"Gawlitza, T.M., Lammich, P., M\u00fcller-Olm, M., Seidl, H., Wenner, A.: Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 199\u2013213. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_15"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-319-94111-0_9","volume-title":"Model Checking Software","author":"JO Gutsfeld","year":"2018","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Nordhoff, B.: A branching time variant of CaRet. In: Gallardo, M.M., Merino, P. (eds.) SPIN 2018. LNCS, vol. 10869, pp. 153\u2013170. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_9"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: Vitter, J.S. (ed.) Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, Dallas, Texas, USA, 23\u201326 May 1998, pp. 224\u2013233. ACM (1998). https:\/\/doi.org\/10.1145\/276698.276748","DOI":"10.1145\/276698.276748"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Lakenbrink, R., M\u00fcller-Olm, M., Ohrem, C., Gutsfeld, J.: A navigation logic for recursive programs with dynamic thread creation (2023). https:\/\/arxiv.org\/abs\/2310.19579","DOI":"10.1007\/978-3-031-50521-8_3"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-38856-9_25","volume-title":"Static Analysis","author":"P Lammich","year":"2013","unstructured":"Lammich, P., M\u00fcller-Olm, M., Seidl, H., Wenner, A.: Contextual locking for dynamic pushdown networks. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 477\u2013498. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_25"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-642-02658-4_39","volume-title":"Computer Aided Verification","author":"P Lammich","year":"2009","unstructured":"Lammich, P., M\u00fcller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 525\u2013539. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_39"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-540-30579-8_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Lange","year":"2005","unstructured":"Lange, M.: Weak automata for the linear time $$\\mu $$-Calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 267\u2013281. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_18"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Deusen, M.S.V., Galil, Z., Reid, B.K. (eds.) Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA, January 1985, pp. 97\u2013107. ACM Press (1985). https:\/\/doi.org\/10.1145\/318593.318622","DOI":"10.1145\/318593.318622"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C.: Automata on infinite trees. In: Pin, J. (ed.) Handbook of Automata Theory, pp. 265\u2013302. European Mathematical Society Publishing House, Z\u00fcrich (2021). https:\/\/doi.org\/10.4171\/Automata-1\/8","DOI":"10.4171\/Automata-1\/8"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Nordhoff, B., M\u00fcller-Olm, M., Lammich, P.: Iterable forward reachability analysis of Monitor-DPNs. In: Banerjee, A., Danvy, O., Doh, K., Hatcliff, J. (eds.) Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Manhattan, Kansas, USA, 19\u201320th September 2013. EPTCS, vol. 129, pp. 384\u2013403 (2013). https:\/\/doi.org\/10.4204\/EPTCS.129.24","DOI":"10.4204\/EPTCS.129.24"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Automata, Languages and Programming","author":"A Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652\u2013671. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0035790"},{"issue":"2","key":"3_CR26","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s00165-014-0330-y","volume":"27","author":"F Song","year":"2015","unstructured":"Song, F., Touili, T.: Model checking dynamic pushdown networks. Formal Aspects Comput. 27(2), 397\u2013421 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0330-y","journal-title":"Formal Aspects Comput."},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5(2), 285\u2013309 (1955). https:\/\/projecteuclid.org:443\/euclid.pjm\/1103044538","DOI":"10.2140\/pjm.1955.5.285"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: POPL, pp. 250\u2013259. ACM Press (1988). https:\/\/doi.org\/10.1145\/73560.735822","DOI":"10.1145\/73560.735822"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Automata, Languages and Programming","author":"MY Vardi","year":"1998","unstructured":"Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628\u2013641. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055090"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-50521-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:07:45Z","timestamp":1704240465000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-50521-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,30]]},"ISBN":["9783031505201","9783031505218"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-50521-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023,12,30]]},"assertion":[{"value":"30 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/VMCAI-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"74","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}