{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:50:20Z","timestamp":1743033020194,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030451899"},{"type":"electronic","value":"9783030451905"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45190-5_21","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T09:03:02Z","timestamp":1587114182000},"page":"387-404","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Revisiting Underapproximate Reachability for Multipushdown Systems"],"prefix":"10.1007","author":[{"given":"S.","family":"Akshay","sequence":"first","affiliation":[]},{"given":"Paul","family":"Gastin","sequence":"additional","affiliation":[]},{"given":"S","family":"Krishna","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3583-7612","authenticated-orcid":false,"given":"Sparsa","family":"Roychowdhury","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. p. 35\u201344 (2012), \nhttps:\/\/doi.org\/10.1109\/LICS.2012.15","key":"21_CR1","DOI":"10.1109\/LICS.2012.15"},{"doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Stenman, J.: The minimal cost reachability problem in priced timed pushdown systems. In: Language and Automata Theory and Applications - 6th International Conference, LATA 2012, A Coru\u00f1a, Spain, March 5-9, 2012. Proceedings. pp. 58\u201369 (2012), \nhttps:\/\/doi.org\/10.1007\/978-3-642-28332-1_6","key":"21_CR2","DOI":"10.1007\/978-3-642-28332-1_6"},{"unstructured":"Akshay, S., Gastin, P., Jug\u00e9, V., Krishna, S.N.: Timed systems through the lens of logic. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. pp. 1\u201313 (2019)","key":"21_CR3"},{"unstructured":"Akshay, S., Gastin, P., Krishna, S., Roychowdhury, S.: Revisiting underapproximate reachability for multipushdown systems (2020), \nhttps:\/\/arxiv.org\/abs\/2002.05950","key":"21_CR4"},{"unstructured":"Akshay, S., Gastin, P., Krishna, S.N.: Analyzing Timed Systems Using Tree Automata. Logical Methods in Computer Science Volume 14, Issue 2 (May 2018), \nhttps:\/\/lmcs.episciences.org\/4489","key":"21_CR5"},{"unstructured":"Akshay, S., Gastin, P., Krishna, S.N., Sarkar, I.: Towards an efficient tree automata based technique for timed systems. In: 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany. pp. 39:1\u201339:15 (2017), \nhttps:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2017.39","key":"21_CR6"},{"doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing. pp. 202\u2013211. ACM (2004)","key":"21_CR7","DOI":"10.1145\/1007352.1007390"},{"doi-asserted-by":"publisher","unstructured":"Atig, M.F.: Model-Checking of Ordered Multi-Pushdown Automata. Logical Methods in Computer Science Volume 8, Issue 3 (Sep 2012). \nhttps:\/\/doi.org\/10.2168\/LMCS-8(3:20)2012","key":"21_CR8","DOI":"10.2168\/LMCS-8(3:20)2012"},{"doi-asserted-by":"crossref","unstructured":"Bhave, D., Dave, V., Krishna, S.N., Phawade, R., Trivedi, A.: A perfect class of context-sensitive timed languages. In: International Conference on Developments in Language Theory. pp. 38\u201350. Springer, Berlin, Heidelberg (2016)","key":"21_CR9","DOI":"10.1007\/978-3-662-53132-7_4"},{"doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: International Hybrid Systems Workshop. pp. 64\u201385. Springer (1994)","key":"21_CR10","DOI":"10.1007\/3-540-60472-3_4"},{"doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. p. 334\u2013349. Springer (2006)","key":"21_CR11","DOI":"10.1007\/11691372_22"},{"unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. MIT press (2009)","key":"21_CR12"},{"unstructured":"Cyriac, A.: Verification of communicating recursive programs via split-width. (V\u00e9rification de programmes r\u00e9cursifs et communicants via split-width). Ph.D. thesis, \u00c9cole normale sup\u00e9rieure de Cachan, France (2014), \nhttps:\/\/tel.archives-ouvertes.fr\/tel-01015561","key":"21_CR13"},{"doi-asserted-by":"crossref","unstructured":"Cyriac, A., Gastin, P., Kumar, K.N.: MSO decidability of multi-pushdown systems via split-width. In: International Conference on Concurrency Theory. pp. 547\u2013561. Springer, Berlin, Heidelberg (2012)","key":"21_CR14","DOI":"10.1007\/978-3-642-32940-1_38"},{"doi-asserted-by":"crossref","unstructured":"Dang, Z., Ibarra, O.H., Bultan, T., Kemmerer, R.A., Su, J.: Binary reachability analysis of discrete pushdown timed automata. In: International Conference on Computer Aided Verification. p. 69\u201384. Springer (2000)","key":"21_CR15","DOI":"10.1007\/10722167_9"},{"doi-asserted-by":"crossref","unstructured":"Hague, M., Lin, A.W.: Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. p. 260\u2013276 (2012), \nhttps:\/\/doi.org\/10.1007\/978-3-642-31424-7_22","key":"21_CR16","DOI":"10.1007\/978-3-642-31424-7_22"},{"doi-asserted-by":"crossref","unstructured":"Kung, H., Lehman, P.L.: Concurrent manipulation of binary search trees. ACM Transactions on Database Systems (TODS) 5(3), 354\u2013382 (1980)","key":"21_CR17","DOI":"10.1145\/320613.320619"},{"doi-asserted-by":"crossref","unstructured":"La\u00a0Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium on. pp. 161\u2013170. IEEE (2007)","key":"21_CR18","DOI":"10.1109\/LICS.2007.9"},{"doi-asserted-by":"crossref","unstructured":"La\u00a0Torre, S., Madhusudan, P., Parlato, G.: The language theory of bounded context-switching. In: Latin American Symposium on Theoretical Informatics. pp. 96\u2013107. Springer (2010)","key":"21_CR19","DOI":"10.1007\/978-3-642-12200-2_10"},{"doi-asserted-by":"crossref","unstructured":"La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: International Conference on Concurrency Theory. p. 203\u2013218. Springer (2011)","key":"21_CR20","DOI":"10.1007\/978-3-642-23217-6_14"},{"doi-asserted-by":"crossref","unstructured":"La\u00a0Torre, S., Parthasarathy, M., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. ACM Sigplan Notices 44(6), 211\u2013222 (2009)","key":"21_CR21","DOI":"10.1145\/1543135.1542500"},{"doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: ACM SIGPLAN Notices. vol.\u00a046, pp. 283\u2013294. ACM (2011)","key":"21_CR22","DOI":"10.1145\/1925844.1926419"},{"doi-asserted-by":"crossref","unstructured":"Patin, G., Sighireanu, M., Touili, T.: Spade: Verification of multithreaded dynamic and recursive programs. In: International Conference on Computer Aided Verification. pp. 254\u2013257. Springer (2007)","key":"21_CR23","DOI":"10.1007\/978-3-540-73368-3_28"},{"doi-asserted-by":"crossref","unstructured":"Qadeer, S.: The case for context-bounded verification of concurrent programs. In: Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings. pp.\u00a03\u20136 (2008), \nhttps:\/\/doi.org\/10.1007\/978-3-540-85114-1_2","key":"21_CR24","DOI":"10.1007\/978-3-540-85114-1_2"},{"doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. ACM sigplan notices 39(6), 14\u201324 (2004)","key":"21_CR25","DOI":"10.1145\/996893.996845"},{"unstructured":"Silberschatz, A., Gagne, G., Galvin, P.B.: Operating system concepts. Wiley (2018)","key":"21_CR26"},{"doi-asserted-by":"crossref","unstructured":"Torre, S.L., Napoli, M., Parlato, G.: Scope-bounded pushdown languages. International Journal of Foundations of Computer Science 27(02), 215\u2013233 (2016)","key":"21_CR27","DOI":"10.1142\/S0129054116400074"},{"doi-asserted-by":"publisher","unstructured":"Torre, S.L., Parlato, G.: Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width 18, 173\u2013184 (2012). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.173","key":"21_CR28","DOI":"10.4230\/LIPIcs.FSTTCS.2012.173"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45190-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,20]],"date-time":"2020-08-20T13:14:49Z","timestamp":1597929289000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","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":"155","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":"40","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":"8","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":"26% - 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":"14","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)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}