{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:32Z","timestamp":1760202632663,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642237010"},{"type":"electronic","value":"9783642237027"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-23702-7_13","type":"book-chapter","created":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T17:31:31Z","timestamp":1315589491000},"page":"129-145","source":"Crossref","is-referenced-by-count":19,"title":["On Sequentializing Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[]},{"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: Analyzing asynchronous programs with preemption. In: FSTTCS 2008: Proc. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. LIPIcs, vol.\u00a02, pp. 37\u201348. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-00768-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.F. Atig","year":"2009","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 107\u2013123. Springer, Heidelberg (2009)"},{"key":"13_CR3","first-page":"1","volume-title":"POPL 2002: Proc. 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: POPL 2002: Proc. 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1\u20133. ACM, New York (2002)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Parlato, G.: On sequentializing concurrent programs (2011), http:\/\/hal.archives-ouvertes.fr\/hal-00597415\/en\/","DOI":"10.1007\/978-3-642-23702-7_13"},{"key":"13_CR5","first-page":"159","volume-title":"POPL 2008: Proc. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"S. Chaudhuri","year":"2008","unstructured":"Chaudhuri, S.: Subcubic algorithms for recursive state machines. In: POPL 2008: Proc. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 159\u2013169. ACM, New York (2008)"},{"key":"13_CR6","first-page":"238","volume-title":"POPL 1977: Proc. 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Proc. 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM, New York (1977)"},{"key":"13_CR7","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Emmi, M., Qadeer, S., Rakamari\u0107, Z.: Delay-bounded scheduling. In: POPL 2011: Proc. 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 411\u2013422. ACM, New York (2011)","DOI":"10.1145\/1926385.1926432"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-642-14295-6_52","volume-title":"Computer Aided Verification","author":"P. Ganty","year":"2010","unstructured":"Ganty, P., Majumdar, R., Monmege, B.: Bounded underapproximations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 600\u2013614. Springer, Heidelberg (2010)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-19835-9_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Garg","year":"2011","unstructured":"Garg, P., Madhusudan, P.: Compositionality entails sequentializability. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 26\u201340. Springer, Heidelberg (2011)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-16164-3_17","volume-title":"Model Checking Software","author":"N. Ghafari","year":"2010","unstructured":"Ghafari, N., Hu, A.J., Rakamari\u0107, Z.: Context-bounded translations for concurrent software: An empirical evaluation. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol.\u00a06349, pp. 227\u2013244. Springer, Heidelberg (2010)"},{"key":"13_CR12","unstructured":"Jannet, B., Min\u00e9, A.: The Interproc analyzer, http:\/\/pop-art.inrialpes.fr\/interproc\/interprocweb.cgi"},{"key":"13_CR13","unstructured":"Kahlon, V.: Tractable dataflow analysis for concurrent programs via bounded languages, Patent WO\/2009\/094439 (July 2009)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-16164-3_18","volume-title":"Model Checking Software","author":"N. Kidd","year":"2010","unstructured":"Kidd, N., Jagannathan, S., Vitek, J.: One stack to run them all: Reducing concurrent analysis to sequential analysis under priority scheduling. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol.\u00a06349, pp. 245\u2013261. Springer, Heidelberg (2010)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-02658-4_36","volume-title":"Computer Aided Verification","author":"S. Torre La","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 477\u2013492. Springer, Heidelberg (2009)"},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/1542476.1542500","volume-title":"PLDI 2009: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"S. La Torre","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: PLDI 2009: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 211\u2013222. ACM, New York (2009)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/978-3-642-14295-6_54","volume-title":"Computer Aided Verification","author":"S. La Torre","year":"2010","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 629\u2013644. Springer, Heidelberg (2010)"},{"key":"13_CR18","first-page":"171","volume-title":"POPL 2008: Proc. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"S.K. Lahiri","year":"2008","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: POPL 2008: Proc. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 171\u2013182. ACM, New York (2008)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-02658-4_38","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 509\u2013524. Springer, Heidelberg (2009)"},{"issue":"1","key":"13_CR20","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A. Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design\u00a035(1), 73\u201397 (2009)","journal-title":"Formal Methods in System Design"},{"key":"13_CR21","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/1250734.1250785","volume-title":"PLDI 2007: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI 2007: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 446\u2013455. ACM, New York (2007)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"13_CR23","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/996841.996845","volume-title":"PLDI 2004: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Wu, D.: KISS: Keep it simple and sequential. In: PLDI 2004: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 14\u201324. ACM, New York (2004)"},{"key":"13_CR24","first-page":"49","volume-title":"POPL 1995: Proc. 22th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"T.W. Reps","year":"1995","unstructured":"Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995: Proc. 22th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 49\u201361. ACM, New York (1995)"},{"issue":"1-2","key":"13_CR25","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T.W. Reps","year":"2005","unstructured":"Reps, T.W., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program.\u00a058(1-2), 206\u2013263 (2005)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23702-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,15]],"date-time":"2019-06-15T03:03:13Z","timestamp":1560567793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23702-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237010","9783642237027"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23702-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}