{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:15:58Z","timestamp":1770977758954,"version":"3.50.1"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,4,25]],"date-time":"2014-04-25T00:00:00Z","timestamp":1398384000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1007\/s10703-014-0207-y","type":"journal-article","created":{"date-parts":[[2014,4,24]],"date-time":"2014-04-24T09:00:20Z","timestamp":1398330020000},"page":"273-301","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Budget-bounded model-checking pushdown systems"],"prefix":"10.1007","volume":"45","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Othmane","family":"Rezine","sequence":"additional","affiliation":[]},{"given":"Jari","family":"Stenman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,25]]},"reference":[{"key":"207_CR1","unstructured":"Abdulla PA, Atig MF, Rezine O, Stenman J (2012) Multi-pushdown systems with budgets. In: Cabodi G, Singh S (eds) FMCAD. IEEE, pp 24\u201333"},{"key":"207_CR2","unstructured":"Atig MF, Bollig B, Habermehl P (2008) Emptiness of multi-pushdown automata is $$2$$ 2 ETIME-complete. In: DLT\u201908, LNCS, vol 5257. Springer, Berlin, pp 121\u2013133"},{"key":"207_CR3","doi-asserted-by":"crossref","unstructured":"Atig MF, Bouajjani A, Emmi M, Lal A (2012) Detecting fair non-termination in multithreaded programs. In: Madhusudan P, S. A. Seshia (eds) CAV, lecture notes in computer science, vol 7358, pp 210\u2013226","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"207_CR4","first-page":"152","volume-title":"ATVA, lecture notes in computer science","author":"MF Atig","year":"2012","unstructured":"Atig MF, Bouajjani A, Kumar KN, Saivasan P (2012) Linear-time model-checking for multithreaded programs under scope-bounding. In: Chakraborty S, Mukund M (eds) ATVA, lecture notes in computer science. Springer, Berlin, pp 152\u2013166"},{"key":"207_CR5","doi-asserted-by":"crossref","unstructured":"Atig MF, Kumar KN, Saivasan P (2013) Adjacent ordered multi-pushdown systems. In: B\u00e9al MP, Carton O (eds) Developments in language theory, lecture notes in computer science. Springer, Berlin, pp 58\u201369","DOI":"10.1007\/978-3-642-38771-5_7"},{"key":"207_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Emmi M, Parlato G (2011) On sequentializing concurrent programs. In: SAS \u201911, proceedings of the 18th international symposium on static analysis. Springer, Berlin, pp 129\u2013145","DOI":"10.1007\/978-3-642-23702-7_13"},{"key":"207_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Esparza J, Maler O (1997) Reachability analysis of pushdown automata: application to model-checking. In: CONCUR, LNCS, vol 1243. Springer, Berlin, pp 135\u2013150","DOI":"10.1007\/3-540-63141-0_10"},{"key":"207_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Maler O (1996) Reachability analysis of pushdown automata. In: Proceedings of international workshop on verification of infinite-state systems (Infinity\u201996)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"207_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani A, M\u00fcller-Olm M, Touili T (2005) Regular symbolic analysis of dynamic networks of pushdown systems. In: CONCUR\u201905, LNCS","DOI":"10.1007\/11539452_36"},{"issue":"3","key":"207_CR10","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1142\/S0129054196000191","volume":"7","author":"L Breveglieri","year":"1996","unstructured":"Breveglieri L, Cherubini A, Citrini C, Crespi Reghizzi S (1996) Multi-push-down languages and grammars. Int J Found Comput Sci 7(3):253\u2013292","journal-title":"Int J Found Comput Sci"},{"key":"207_CR11","doi-asserted-by":"crossref","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS, LNCS vol 2988, pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"207_CR12","unstructured":"Cordeiro L, Morse J, Nicole D, Fischer B (2012) Context-bounded model checking with esbmc 1.17\u2014(competition contribution). In: TACAS, LNCS, vol 7214, pp 534\u2013537"},{"key":"207_CR13","volume-title":"Automata, languages, and machines","author":"S Eilenberg","year":"1974","unstructured":"Eilenberg S (1974) Automata, languages, and machines. Academic Press Inc, Orlando, FL"},{"key":"207_CR14","doi-asserted-by":"crossref","unstructured":"Emmi M, Qadeer S, Rakamari\u0107 Z (2011) Delay-bounded scheduling. In: POPL. ACM, pp 411\u2013422","DOI":"10.1145\/1926385.1926432"},{"key":"207_CR15","unstructured":"Esbmc concurrency benchmark (2009)"},{"key":"207_CR16","doi-asserted-by":"crossref","unstructured":"Esparza J, Kiefer S, Schwoon S (2006) Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: TACAS, LNCS vol 3920, pp 489\u2013503","DOI":"10.1007\/11691372_35"},{"key":"207_CR17","doi-asserted-by":"crossref","unstructured":"Finkel A, Sangnier A (2008) Reversal-bounded counter machines revisited. In: MFCS, LNCS, vol 5162. Springer, Berlin, pp 323\u2013334","DOI":"10.1007\/978-3-540-85238-4_26"},{"key":"207_CR18","volume-title":"Algebraic and automata-theoretic properties of formal languages","author":"S Ginsburg","year":"1975","unstructured":"Ginsburg S (1975) Algebraic and automata-theoretic properties of formal languages. Elsevier Science Inc., New York, NY"},{"key":"207_CR19","volume-title":"Introduction to formal language theory","author":"M Harrison","year":"1978","unstructured":"Harrison M (1978) Introduction to formal language theory. Addison-Wesley Publishing Company, Reading, MA"},{"key":"207_CR20","volume-title":"The art of multiprocessor programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, Los Altos, CA"},{"key":"207_CR21","volume-title":"Introduction to automata theory, languages and computation","author":"JE Hopcroft","year":"1979","unstructured":"Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages and computation. Addison-Wesley, Reading, MA"},{"key":"207_CR22","unstructured":"http:\/\/user.it.uu.se\/jarst116\/fmcad2012\/ (2012)"},{"key":"207_CR23","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2007) A robust class of context-sensitive languages. In: LICS. IEEE, pp 161\u2013170","DOI":"10.1109\/LICS.2007.9"},{"key":"207_CR24","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2009) Reducing context-bounded concurrent reachability to sequential reachability. In: CAV, LNCS, vol 5643. Springer, Berlin, pp 477\u2013492","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"207_CR25","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2010) Model-checking parameterized concurrent programs using linear interfaces. In: CAV, LNCS, vol 6174. Springer, Berlin, pp 629\u2013644","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"207_CR26","unstructured":"La Torre S, Napoli M (2011) Reachability of multistack pushdown systems with scope-bounded matching relations. In: CONCUR, LNCS, vol 6901. Springer, Berlin, pp 203\u2013218"},{"key":"207_CR27","unstructured":"La Torre S, Parlato G (2012) Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. Technical report, University of Southampton"},{"key":"207_CR28","unstructured":"Lahiri S, Lal A, Qadeer S (2012) Poirot microsoft research. http:\/\/research.microsoft.com\/en-us\/projects\/verifierq\/"},{"key":"207_CR29","doi-asserted-by":"crossref","unstructured":"Lal A, Reps T (2008) Reducing concurrent analysis under a context bound to sequential analysis. In: CAV, LNCS, vol 5123. Springer, Berlin, pp 37\u201351","DOI":"10.1007\/978-3-540-70545-1_7"},{"issue":"1","key":"207_CR30","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal A, Reps TW (2009) Reducing concurrent analysis under a context bound to sequential analysis. Form Methods Syst Des 35(1):73\u201397","journal-title":"Form Methods Syst Des"},{"key":"207_CR31","unstructured":"Lange M, Lei H (2009) To CNF or not to CNF ? An efficient yet presentable version of the CYK algorithm. Inf Didact 8:2008\u20132009"},{"key":"207_CR32","unstructured":"Morse J Personal communication"},{"key":"207_CR33","doi-asserted-by":"crossref","unstructured":"Musuvathi M, Qadeer S (2007) Iterative context bounding for systematic testing of multithreaded programs. In: PLDI. ACM, pp 446\u2013455","DOI":"10.1145\/1250734.1250785"},{"key":"207_CR34","unstructured":"Parlato G Personal communication"},{"key":"207_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: FOCS. IEEE, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"207_CR36","doi-asserted-by":"crossref","unstructured":"Qadeer S, Rajamani SK, Rehof J (2004) Summarizing procedures in concurrent programs. In: ACM SIGPLAN Notices, vol 39, pp 245\u2013255","DOI":"10.1145\/964001.964022"},{"key":"207_CR37","doi-asserted-by":"crossref","unstructured":"Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: TACAS, LNCS, vol 3440. Springer, Berlin, pp 93\u2013107","DOI":"10.1007\/978-3-540-31980-1_7"},{"issue":"2","key":"207_CR38","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G Ramalingam","year":"2000","unstructured":"Ramalingam G (2000) Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans Program Lang Syst 22(2):416\u2013430","journal-title":"ACM Trans Program Lang Syst"},{"key":"207_CR39","doi-asserted-by":"crossref","unstructured":"Sen K, Viswanathan M (2006) Model checking multithreaded programs with asynchronous atomic methods. In: CAV. LNCS 4144, pp 300\u2013314","DOI":"10.1007\/11817963_29"},{"key":"207_CR40","unstructured":"Suwimonteerabuth D (2009) Reachability in pushdown systems: algorithms and applications. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen"},{"key":"207_CR41","doi-asserted-by":"crossref","unstructured":"Vardi MY (1988) A temporal fixpoint calculus. In: POPL, pp 250\u2013259","DOI":"10.1145\/73560.73582"},{"key":"207_CR42","doi-asserted-by":"crossref","unstructured":"Vardi MY (1995) Alternating automata and program verification. In: Computer science today, lecture notes in computer science, vol 1000. Springer, Berlin, pp 471\u2013485","DOI":"10.1007\/BFb0015261"},{"key":"207_CR43","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: LICS. IEEE Computer Society LICS, pp 332\u2013344"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0207-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0207-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0207-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:58:17Z","timestamp":1746197897000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0207-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,25]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["207"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0207-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,25]]}}}