{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:52Z","timestamp":1767929272949,"version":"3.49.0"},"reference-count":28,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,11,23]],"date-time":"2011-11-23T00:00:00Z","timestamp":1322006400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Context-bounded analysis has been shown to be both efficient and effective at\nfinding bugs in concurrent programs. According to its original definition,\ncontext-bounded analysis explores all behaviors of a concurrent program up to\nsome fixed number of context switches between threads. This definition is\ninadequate for programs that create threads dynamically because bounding the\nnumber of context switches in a computation also bounds the number of threads\ninvolved in the computation. In this paper, we propose a more general\ndefinition of context-bounded analysis useful for programs with dynamic thread\ncreation. The idea is to bound the number of context switches for each thread\ninstead of bounding the number of switches of all threads. We consider several\nvariants based on this new definition, and we establish decidability and\ncomplexity results for the analysis induced by them.<\/jats:p>","DOI":"10.2168\/lmcs-7(4:4)2011","type":"journal-article","created":{"date-parts":[[2012,6,20]],"date-time":"2012-06-20T09:05:51Z","timestamp":1340183151000},"source":"Crossref","is-referenced-by-count":26,"title":["Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads"],"prefix":"10.46298","volume":"Volume 7, Issue 4","author":[{"given":"Mohamed Faouzi","family":"Atig","sequence":"first","affiliation":[]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2011,11,23]]},"reference":[{"key":"10.2168\/LMCS-7(4:4)2011_BESS05","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek. Reachability analysis of multithreaded software with asynchronous communication. InFSTTCS'05, LNCS 3821, pages 348-359. Springer, 2005.","DOI":"10.1007\/11590156_28"},{"key":"10.2168\/LMCS-7(4:4)2011_BMOT05","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Markus M\u00fcller-Olm, and Tayssir Touili. Regular symbolic analysis of dynamic networks of pushdown systems. InCONCUR'05, LNCS, 2005.","DOI":"10.1007\/11539452_36"},{"key":"10.2168\/LMCS-7(4:4)2011_BT03","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani and Tayssir Touili. Reachability Analysis of Process Rewrite Systems. InFSTTCS'03. LNCS 2914, 2003.","DOI":"10.1007\/978-3-540-24597-1_7"},{"key":"10.2168\/LMCS-7(4:4)2011_BT05","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani and Tayssir Touili. On Computing Reachability Sets of Process Rewrite Systems. InRTA'05. LNCS, 2005.","DOI":"10.1007\/978-3-540-32033-3_35"},{"key":"10.2168\/LMCS-7(4:4)2011_CKS06","first-page":"53","author":"Byron Cook, Daniel Kroening, and Natasha","year":"2006","journal-title":"Formal Methods in Computer Aided Design"},{"issue":"1-3","key":"10.2168\/LMCS-7(4:4)2011_CKS07","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2007.07.050","volume":"388","author":"Byron Cook, Daniel Kroening, and Natasha","year":"2007","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-7(4:4)2011_Cour91","first-page":"178","volume":"44","author":"Bruno Courcelle","year":"1991","journal-title":"EATCS'91"},{"key":"10.2168\/LMCS-7(4:4)2011_EP00","doi-asserted-by":"crossref","unstructured":"J. Esparza and A. Podelski. Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. InPOPL'00. ACM, 2000.","DOI":"10.1145\/325694.325697"},{"key":"10.2168\/LMCS-7(4:4)2011_GRVB06","doi-asserted-by":"crossref","unstructured":"P. Ganty, J. F. Raskin, and L. Van Begin. A complete abstract interpretation framework for coverability properties of WSTS. InVMCAI'06, LNCS 3855, pages 49-64. Springer, 2006.","DOI":"10.1007\/11609773_4"},{"issue":"1","key":"10.2168\/LMCS-7(4:4)2011_GRB06","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1016\/j.jcss.2005.09.001","volume":"72","author":"G. Geeraerts, J. F. Raskin, and L. Van B","year":"2006","journal-title":"J. Comput. Syst. Sci."},{"key":"10.2168\/LMCS-7(4:4)2011_HU79","unstructured":"John E. Hopcroft and Jeffrey D. Ullman.Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979."},{"key":"10.2168\/LMCS-7(4:4)2011_lipton","unstructured":"R. Lipton. The reachability problem requires exponential time. Technical Report TR 66, 1976."},{"key":"10.2168\/LMCS-7(4:4)2011_TMP09","doi-asserted-by":"crossref","unstructured":"Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Reducing context-bounded concurrent reachability to sequential reachability. InCAV}, volume 5643 ofLecture Notes in Computer Science, pages 477-492. Springer, 2009.","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"10.2168\/LMCS-7(4:4)2011_LR08","doi-asserted-by":"crossref","unstructured":"A. Lal and T. W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. InCAV'08, LNCS 5123, pages 37-51. Springer, 2008.","DOI":"10.1007\/978-3-540-70545-1_7"},{"key":"10.2168\/LMCS-7(4:4)2011_LS98","unstructured":"D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PA-processes. InProc. 9th Int. Conf. Concurrency Theory (CONCUR'98), Nice, France, Sep. 1998, volume 1466, pages 50-66. Springer, 1998."},{"key":"10.2168\/LMCS-7(4:4)2011_LTKR08","doi-asserted-by":"crossref","unstructured":"A. Lal, T. Touili, N. Kidd, and T. W. Reps. Interprocedural analysis of concurrent programs under a context bound. InTACAS'08, LNCS 4963, pages 282-298. Springer, 2008.","DOI":"10.1007\/978-3-540-78800-3_20"},{"key":"10.2168\/LMCS-7(4:4)2011_Markus","unstructured":"M. Muller-olm. Variations on constants. Habilitation thesis, Dortmund University, 2002."},{"key":"10.2168\/LMCS-7(4:4)2011_MQ07","doi-asserted-by":"crossref","unstructured":"M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. InPLDI'07, pages 446-455. ACM, 2007.","DOI":"10.1145\/1250734.1250785"},{"key":"10.2168\/LMCS-7(4:4)2011_QR05","doi-asserted-by":"crossref","unstructured":"S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. InTACAS'05, LNCS 3440, pages 93-107. Springer, 2005.","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"10.2168\/LMCS-7(4:4)2011_QW04","doi-asserted-by":"crossref","unstructured":"S. Qadeer and D. Wu. KISS: keep it simple and sequential. InPLDI'04, pages 14-24. ACM, 2004.","DOI":"10.1145\/996841.996845"},{"key":"10.2168\/LMCS-7(4:4)2011_Rackoff78","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"Charles Rackoff","year":"1978","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"10.2168\/LMCS-7(4:4)2011_Ram00","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.2168\/LMCS-7(4:4)2011_SES08","doi-asserted-by":"crossref","unstructured":"D. Suwimonteerabuth, J. Esparza, and S. Schwoon. Symbolic context-bounded analysis of multithreaded java programs. InSPIN'08, LNCS 5156, pages 270-287. Springer, 2008.","DOI":"10.1007\/978-3-540-85114-1_19"},{"key":"10.2168\/LMCS-7(4:4)2011_SS00","doi-asserted-by":"crossref","unstructured":"Helmut Seidl and Bernhard Steffen. Constraint-based inter-procedural analysis of parallel programs. In9th European Symposium on Programming (ESOP), 2000.","DOI":"10.1007\/3-540-46425-5_23"},{"key":"10.2168\/LMCS-7(4:4)2011_SSMH04","doi-asserted-by":"crossref","unstructured":"H. Seidl, T. Schwentick, A. Muscholl, and P. Habermehl. Counting in trees for free. InICALP'04, LNCS 3142, pages 1136-1149. Springer, 2004.","DOI":"10.1007\/978-3-540-27836-8_94"},{"issue":"1","key":"10.2168\/LMCS-7(4:4)2011_Ste95","doi-asserted-by":"crossref","first-page":"91","DOI":"10.3233\/FI-1995-2314","volume":"23","author":"Iain A. Stewart","year":"1995","journal-title":"Fundam. Inform."},{"key":"10.2168\/LMCS-7(4:4)2011_VSS05","doi-asserted-by":"crossref","unstructured":"Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the complexity of equational Horn clauses. InCADE'05, LNCS 3632, pages 337-352. Springer, 2005.","DOI":"10.1007\/11532231_25"},{"key":"10.2168\/LMCS-7(4:4)2011_ZJ08","doi-asserted-by":"crossref","unstructured":"A. Zaks and R. Joshi. Verifying multi-threaded C programs with SPIN. InSPIN'08, LNCS 5156, pages 325-342. Springer, 2008.","DOI":"10.1007\/978-3-540-85114-1_22"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/708\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/708\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:54:15Z","timestamp":1681242855000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/708"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,23]]},"references-count":28,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(4:4)2011","relation":{"references":[{"id-type":"doi","id":"10.1145\/1250734.1250785","asserted-by":"subject"},{"id-type":"doi","id":"10.1145\/1273442.1250785","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1111.1011","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1111.1011","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,23]]},"article-number":"708"}}