{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T12:05:34Z","timestamp":1774440334373,"version":"3.50.1"},"publisher-location":"Cham","reference-count":81,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_18","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"573-611","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Model Checking Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Aarti","family":"Gupta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vineet","family":"Kahlon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"2","key":"18_CR1","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/s10703-011-0135-z","volume":"40","author":"J. Alglave","year":"2012","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models (extended version). Form. Methods Syst. Des. 40(2), 170\u2013205 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"18_CR2","series-title":"LNCS","first-page":"356","volume-title":"CONCUR","author":"M.F. Atig","year":"2008","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR. LNCS, vol.\u00a05201, pp.\u00a0356\u2013371 (2008)"},{"key":"18_CR3","series-title":"LNCS","first-page":"145","volume-title":"CIAA","author":"M.F. Atig","year":"2009","unstructured":"Atig, M.F., Touili, T.: Verifying parallel programs with dynamic communication structures. In: Maneth, S. (ed.) CIAA. LNCS, vol.\u00a05642, pp.\u00a0145\u2013154. Springer, Heidelberg (2009)"},{"issue":"3","key":"18_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(3:21)2013","volume":"9","author":"R. Bonnet","year":"2013","unstructured":"Bonnet, R., Chadha, R., Madhusudan, P., Viswanathan, M.: Reachability under contextual locking. Log. Methods Comput. Sci. 9(3), 1\u201317 (2013)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2","key":"18_CR5","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/s10009-013-0276-z","volume":"16","author":"A. Bouajjani","year":"2014","unstructured":"Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. Int. J. Softw. Tools Technol. Transf. 16(2), 127\u2013146 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"18_CR6","series-title":"LNCS","first-page":"135","volume-title":"CONCUR","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Marzurkiewicz, A., Winkowski, J. (eds.) CONCUR. LNCS, vol.\u00a01243, pp.\u00a0135\u2013150. Springer, Heidelberg (1997)"},{"key":"18_CR7","series-title":"LNCS","first-page":"348","volume-title":"FSTTCS","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Esparza, J., Schwoon, S., Strejcek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Ramanujan, R., Sen, S. (eds.) FSTTCS. LNCS, vol.\u00a03821, pp.\u00a0348\u2013359. Springer, Heidelberg (2005)"},{"key":"18_CR8","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1145\/604131.604137","volume-title":"POPL","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL, pp.\u00a062\u201373. ACM, New York (2003)"},{"issue":"4","key":"18_CR9","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1142\/S0129054103001893","volume":"14","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. Int. J. Found. Comput. Sci. 14(4), 551\u2013582 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"18_CR10","series-title":"LNCS","first-page":"489","volume-title":"CAV","author":"S. Burckhardt","year":"2006","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded model checking of concurrent data types on relaxed memory models: a\u00a0case study. In: Ball, T., Jones, R.B. (eds.) CAV. LNCS, vol.\u00a04144, pp.\u00a0489\u2013502. Springer, Heidelberg (2006)"},{"key":"18_CR11","first-page":"12","volume-title":"PLDI","author":"S. Burckhardt","year":"2007","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Checkfence: checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp.\u00a012\u201321. ACM, New York (2007)"},{"key":"18_CR12","series-title":"LNCS","first-page":"107","volume-title":"CAV","author":"S. Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV. LNCS, vol.\u00a05123, pp.\u00a0107\u2013120. Springer, Heidelberg (2008)"},{"issue":"6","key":"18_CR13","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C. Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)","journal-title":"J. ACM"},{"key":"18_CR14","series-title":"LNCS","first-page":"951","volume-title":"CAV","author":"P. Cern\u00fd","year":"2013","unstructured":"Cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV. LNCS, vol.\u00a08044, pp.\u00a0951\u2013967. Springer, Heidelberg (2013)"},{"key":"18_CR15","series-title":"LNCS","first-page":"437","volume-title":"TACAS","author":"R. Chadha","year":"2012","unstructured":"Chadha, R., Madhusudan, P., Viswanathan, M.: Reachability under contextual locking. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS. LNCS, vol.\u00a07214, pp.\u00a0437\u2013450. Springer, Heidelberg (2012)"},{"key":"18_CR16","series-title":"LNCS","first-page":"334","volume-title":"TACAS","author":"S. Chaki","year":"2006","unstructured":"Chaki, S., Clarke, E.M., Kidd, N., Reps, T.W., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS. LNCS, vol.\u00a03920, pp.\u00a0334\u2013349. Springer, Heidelberg (2006)"},{"key":"18_CR17","series-title":"LNCS","first-page":"240","volume-title":"CAV","author":"F. Chen","year":"2007","unstructured":"Chen, F., Rosu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV. LNCS, vol.\u00a04590, pp.\u00a0240\u2013253. Springer, Heidelberg (2007)"},{"key":"18_CR18","first-page":"304","volume-title":"PLDI","author":"S. Cherem","year":"2008","unstructured":"Cherem, S., Chilimbi, T.M., Gulwani, S.: Inferring locks for atomic sections. In: PLDI, pp.\u00a0304\u2013315. ACM, New York (2008)"},{"key":"18_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, pp.\u00a052\u201371. Springer, Heidelberg (1981)"},{"issue":"2","key":"18_CR20","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/s10703-008-0063-8","volume":"34","author":"A. Cohen","year":"2009","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. Form. Methods Syst. Des. 34(2), 104\u2013125 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"18_CR21","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/1480881.1480885","volume-title":"POPL","author":"T. Elmas","year":"2009","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp.\u00a02\u201315. ACM, New York (2009)"},{"key":"18_CR22","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1145\/1190216.1190260","volume-title":"POPL","author":"M. Emmi","year":"2007","unstructured":"Emmi, M., Fischer, J.S., Jhala, R., Majumdar, R.: Lock allocation. In: POPL, pp.\u00a0291\u2013296. ACM, New York (2007)"},{"key":"18_CR23","series-title":"LNCS","first-page":"324","volume-title":"CAV","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Common, N., Finkel, A. (eds.) CAV. LNCS, vol.\u00a02102, pp.\u00a0324\u2013336. Springer, Heidelberg (2001)"},{"key":"18_CR24","series-title":"LNCS","first-page":"253","volume-title":"SAS","author":"A. Farzan","year":"2010","unstructured":"Farzan, A., Kincaid, Z.: Compositional bitvector analysis for concurrent programs with nested locks. In: Cousot, R., Martel, M. (eds.) SAS. LNCS, vol.\u00a06337, pp.\u00a0253\u2013270. Springer, Heidelberg (2010)"},{"key":"18_CR25","series-title":"LNCS","first-page":"248","volume-title":"CAV","author":"A. Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P., Sorrentino, F.: Meta-analysis for atomicity violations under nested locking. In: Bonajjani, A., Maler, O. (eds.) CAV. LNCS, vol.\u00a05643, pp.\u00a0248\u2013262. Springer, Heidelberg (2009)"},{"key":"18_CR26","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1145\/1040305.1040315","volume-title":"POPL","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp.\u00a0110\u2013121. ACM, New York (2005)"},{"key":"18_CR27","series-title":"LNCS","first-page":"114","volume-title":"SPIN","author":"M.K. Ganai","year":"2008","unstructured":"Ganai, M.K., Gupta, A.: Efficient modeling of concurrent systems in BMC. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN. LNCS, vol.\u00a05156, pp.\u00a0114\u2013133. Springer, Heidelberg (2008)"},{"key":"18_CR28","series-title":"LNCS","first-page":"68","volume-title":"SPIN","author":"M.K. Ganai","year":"2009","unstructured":"Ganai, M.K., Kundu, S.: Reduction of verification conditions for concurrent system using mutually atomic transactions. In: P\u0103s\u0103reanu, C. (ed.) SPIN. LNCS, vol.\u00a05578, pp.\u00a068\u201387. Springer, Heidelberg (2009)"},{"key":"18_CR29","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"18_CR30","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1145\/263699.263717","volume-title":"POPL","author":"P. Godefroid","year":"1997","unstructured":"Godefroid, P.: Model checking for programming languages using Verisoft. In: POPL, pp.\u00a0174\u2013186. ACM, New York (1997)"},{"key":"18_CR31","first-page":"266","volume-title":"PLDI","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI, pp.\u00a0266\u2013277. ACM, New York (2007)"},{"key":"18_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73370-6_8","volume-title":"SPIN Workshop on Model Checking Software","author":"G. Gueta","year":"2007","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN Workshop on Model Checking Software. LNCS, vol.\u00a04595, pp.\u00a095\u2013112. Springer, Heidelberg (2007)"},{"key":"18_CR33","first-page":"331","volume-title":"POPL","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL, pp.\u00a0331\u2013344. ACM, New York (2011)"},{"key":"18_CR34","first-page":"1","volume-title":"PLDI","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI, pp.\u00a01\u201313. ACM, New York (2004)"},{"key":"18_CR35","first-page":"31","volume-title":"ESEC\/SIGSOFT FSE","author":"T.A. Henzinger","year":"2005","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: ESEC\/SIGSOFT FSE, pp.\u00a031\u201340. ACM, New York (2005)"},{"key":"18_CR36","series-title":"LNCS","first-page":"262","volume-title":"CAV","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt, W.A. Jr., Somenzi, F. (eds.) CAV. LNCS, vol.\u00a02725, pp.\u00a0262\u2013274. Springer, Heidelberg (2003)"},{"key":"18_CR37","first-page":"78","volume":"65","author":"G.J. Holzmann","year":"2005","unstructured":"Holzmann, G.J.: Software model checking with SPIN. Adv. Comput. 65, 78\u2013109 (2005)","journal-title":"Adv. Comput."},{"key":"18_CR38","first-page":"27","volume-title":"LICS","author":"V. Kahlon","year":"2009","unstructured":"Kahlon, V.: Boundedness vs. unboundedness of lock chains: characterizing decidability of pairwise CFL-reachability for threads communicating via locks. In: LICS, pp.\u00a027\u201336. IEEE, Piscataway (2009)"},{"key":"18_CR39","series-title":"LNCS","first-page":"450","volume-title":"CONCUR","author":"V. Kahlon","year":"2011","unstructured":"Kahlon, V.: Reasoning about threads with bounded lock chains. In: Katoen, J., K\u00f6nig, B. (eds.) CONCUR. LNCS, vol.\u00a06901, pp.\u00a0450\u2013465. Springer, Heidelberg (2011)"},{"key":"18_CR40","first-page":"101","volume-title":"LICS","author":"V. Kahlon","year":"2006","unstructured":"Kahlon, V., Gupta, A.: An automata-theoretic approach for model checking threads for LTL properties. In: LICS, pp.\u00a0101\u2013110. IEEE, Piscataway (2006)"},{"key":"18_CR41","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1145\/1190216.1190262","volume-title":"POPL","author":"V. Kahlon","year":"2007","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: POPL, pp.\u00a0303\u2013314. ACM, New York (2007)"},{"key":"18_CR42","series-title":"LNCS","first-page":"505","volume-title":"CAV","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivan\u010di\u0107, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV. LNCS, vol.\u00a03576, pp.\u00a0505\u2013518. Springer, Heidelberg (2005)"},{"key":"18_CR43","series-title":"LNCS","first-page":"124","volume-title":"TACAS","author":"V. Kahlon","year":"2009","unstructured":"Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS. LNCS, vol.\u00a05505, pp.\u00a0124\u2013138. Springer, Heidelberg (2009)"},{"key":"18_CR44","series-title":"LNCS","first-page":"434","volume-title":"CAV","author":"V. Kahlon","year":"2010","unstructured":"Kahlon, V., Wang, C.: Universal causality graphs: a precise happens-before model for detecting bugs in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV. LNCS, vol.\u00a06174, pp.\u00a0434\u2013449. Springer, Heidelberg (2010)"},{"key":"18_CR45","series-title":"LNCS","first-page":"398","volume-title":"CAV","author":"V. Kahlon","year":"2009","unstructured":"Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol.\u00a05643, pp.\u00a0398\u2013413. Springer, Heidelberg (2009)"},{"issue":"1","key":"18_CR46","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10009-010-0159-5","volume":"13","author":"N. Kidd","year":"2011","unstructured":"Kidd, N., Lammich, P., Touili, T., Reps, T.W.: A decision procedure for detecting atomicity violations for communicating processes with locks. Int. J. Softw. Tools Technol. Transf. 13(1), 37\u201360 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"18_CR47","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/2261417.2261438","volume":"43","author":"M. Kuperstein","year":"2012","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. SIGACT News 43(2), 108\u2013123 (2012)","journal-title":"SIGACT News"},{"key":"18_CR48","series-title":"LNCS","first-page":"509","volume-title":"CAV","author":"S.K. Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Rakamaric, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol.\u00a05643, pp.\u00a0509\u2013524. Springer, Heidelberg (2009)"},{"key":"18_CR49","series-title":"LNCS","first-page":"434","volume-title":"CAV","author":"A. Lal","year":"2005","unstructured":"Lal, A., Balakrishnan, G., Reps, T.: Extended weighted pushdown systems. In: Ekessami, K., Rajamani, S.K. (eds.) CAV. LNCS, vol.\u00a03576, pp.\u00a0434\u2013448. Springer, Heidelberg (2005)"},{"key":"18_CR50","series-title":"LNCS","first-page":"37","volume-title":"CAV","author":"A. Lal","year":"2008","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV. LNCS, vol.\u00a05123, pp.\u00a037\u201351. Springer, Heidelberg (2008)"},{"key":"18_CR51","series-title":"LNCS","first-page":"525","volume-title":"CAV","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. LNCS, vol.\u00a05643, pp.\u00a0525\u2013539. Springer, Heidelberg (2009)"},{"issue":"7","key":"18_CR52","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"18_CR53","series-title":"LNCS","first-page":"279","volume-title":"Advances in Petri Nets","author":"A.W. Mazurkiewicz","year":"1986","unstructured":"Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Advances in Petri Nets. LNCS, vol.\u00a0255, pp.\u00a0279\u2013324. Springer, Heidelberg (1986)"},{"key":"18_CR54","series-title":"LNCS","volume-title":"ESOP","author":"A. Min\u00e9","year":"2011","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded critical parallel C programs. In: Bart\u00e9, G. (ed.) ESOP. LNCS, vol.\u00a06602. Springer, Heidelberg (2011)"},{"key":"18_CR55","first-page":"267","volume-title":"OSDI","author":"M. Musuvathi","year":"2008","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing Heisenbugs in concurrent programs. In: OSDI, pp.\u00a0267\u2013280. USENIX Association, Berkeley (2008)"},{"key":"18_CR56","series-title":"LNCS","first-page":"49","volume-title":"CONCUR","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR. LNCS, vol.\u00a03170, pp.\u00a049\u201367. Springer, Heidelberg (2004)"},{"key":"18_CR57","series-title":"LNCS","first-page":"409","volume-title":"CAV","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV. LNCS, vol.\u00a0697, pp.\u00a0409\u2013423. Springer, Heidelberg (1993)"},{"key":"18_CR58","series-title":"LNCS","first-page":"93","volume-title":"TACAS","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L. (eds.) TACAS. LNCS, vol.\u00a03440, pp.\u00a093\u2013107. Springer, Heidelberg (2005)"},{"key":"18_CR59","series-title":"LNCS","first-page":"82","volume-title":"CAV","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV. LNCS, vol.\u00a03576, pp.\u00a082\u201397. Springer, Heidelberg (2005)"},{"key":"18_CR60","first-page":"416","volume-title":"TOPLAS","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. In: TOPLAS, pp.\u00a0416\u2013430. ACM, New York (2000)"},{"key":"18_CR61","series-title":"LNCS","first-page":"189","volume-title":"SAS","author":"T. Reps","year":"2003","unstructured":"Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS. LNCS, vol.\u00a02694, pp.\u00a0189\u2013213. Springer, Heidelberg (2003)"},{"key":"18_CR62","first-page":"337","volume-title":"ESEC\/SIGSOFT FSE","author":"K. Sen","year":"2003","unstructured":"Sen, K., Rosu, G., Agha, G.: Runtime safety analysis of multithreaded programs. In: ESEC\/SIGSOFT FSE, pp.\u00a0337\u2013346. ACM, New York (2003)"},{"key":"18_CR63","series-title":"LNCS","first-page":"527","volume-title":"CAV","author":"R. Singh","year":"2010","unstructured":"Singh, R., Giannakopoulou, D., Pasareanu, C.S.: Learning component interfaces with may and must abstractions. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV. LNCS, vol.\u00a06174, pp.\u00a0527\u2013542. Springer, Heidelberg (2010)"},{"key":"18_CR64","first-page":"6","volume-title":"FMCAD","author":"A. Sinha","year":"2012","unstructured":"Sinha, A., Malik, S., Gupta, A.: Efficient predictive analysis for detecting nondeterminism in multi-threaded programs. In: FMCAD, pp.\u00a06\u201315. IEEE, Piscataway (2012)"},{"key":"18_CR65","first-page":"47","volume-title":"SIGSOFT FSE","author":"N. Sinha","year":"2010","unstructured":"Sinha, N., Wang, C.: Staged concurrent program analysis. In: SIGSOFT FSE, pp.\u00a047\u201356. ACM, New York (2010)"},{"key":"18_CR66","first-page":"423","volume-title":"POPL","author":"N. Sinha","year":"2011","unstructured":"Sinha, N., Wang, C.: On interference abstractions. In: POPL, pp.\u00a0423\u2013434. ACM, New York (2011)"},{"key":"18_CR67","first-page":"136","volume-title":"PLDI","author":"A. Solar-Lezama","year":"2008","unstructured":"Solar-Lezama, A., Jones, C.G., Bod\u00edk, R.: Sketching concurrent data structures. In: PLDI, pp.\u00a0136\u2013148. ACM, New York (2008)"},{"issue":"1","key":"18_CR68","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s10009-002-0077-2","volume":"4","author":"S.D. Stoller","year":"2002","unstructured":"Stoller, S.D.: Model-checking multi-threaded distributed Java programs. Int. J. Softw. Tools Technol. Transf. 4(1), 71\u201391 (2002)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"38\u201339","key":"18_CR69","doi-asserted-by":"publisher","first-page":"3460","DOI":"10.1016\/j.tcs.2010.05.028","volume":"411","author":"T. Touili","year":"2010","unstructured":"Touili, T., Atig, M.F.: Verifying parallel programs with dynamic communication structures. Theor. Comput. Sci. 411(38\u201339), 3460\u20133468 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR70","series-title":"LNCS","first-page":"450","volume-title":"CAV","author":"V. Vafeiadis","year":"2010","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV. LNCS, vol.\u00a06174, pp.\u00a0450\u2013464. Springer, Heidelberg (2010)"},{"key":"18_CR71","series-title":"LNCS","first-page":"491","volume-title":"Advances in Petri Nets","author":"A. Valmari","year":"1989","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets. LNCS, vol.\u00a0483, pp.\u00a0491\u2013515. Springer, Heidelberg (1989)"},{"issue":"2","key":"18_CR72","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Autom. Softw. Eng."},{"key":"18_CR73","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1145\/1504176.1504214","volume-title":"PPOPP","author":"A. Vo","year":"2009","unstructured":"Vo, A., Vakkalanka, S.S., Delisi, M., Gopalakrishnan, G., Kirby, R.M., Thakur, R.: Formal verification of practical MPI programs. In: PPOPP, pp.\u00a0261\u2013270. ACM, New York (2009)"},{"key":"18_CR74","series-title":"LNCS","first-page":"127","volume-title":"FSTTCS","author":"I. Walukiewicz","year":"2000","unstructured":"Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FSTTCS. LNCS, vol.\u00a01974, pp.\u00a0127\u2013138. Springer, Heidelberg (2000)"},{"key":"18_CR75","series-title":"LNCS","first-page":"256","volume-title":"FM","author":"C. Wang","year":"2009","unstructured":"Wang, C., Kundu, S., Ganai, M.K., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: Cavalcanti, A., Dams, D. (eds.) FM. LNCS, vol.\u00a05850, pp.\u00a0256\u2013272. Springer, Heidelberg (2009)"},{"key":"18_CR76","series-title":"LNCS","first-page":"328","volume-title":"TACAS","author":"C. Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M.K., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Esparza, J., Majumdar, R. (eds.) TACAS. LNCS, vol.\u00a06015, pp.\u00a0328\u2013342. Springer, Heidelberg (2010)"},{"key":"18_CR77","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/1985793.1985824","volume-title":"ICSE","author":"C. Wang","year":"2011","unstructured":"Wang, C., Said, M., Gupta, A.: Coverage guided systematic concurrency testing. In: ICSE, pp.\u00a0221\u2013230. ACM, New York (2011)"},{"key":"18_CR78","series-title":"LNCS","first-page":"382","volume-title":"TACAS","author":"C. Wang","year":"2008","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. LNCS, vol.\u00a04963, pp.\u00a0382\u2013396. Springer, Heidelberg (2008)"},{"key":"18_CR79","series-title":"LNCS","first-page":"94","volume-title":"FOSSACS","author":"T. Wies","year":"2010","unstructured":"Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS. LNCS, vol.\u00a06014, pp.\u00a094\u2013108. Springer, Heidelberg (2010)"},{"key":"18_CR80","series-title":"LNCS","first-page":"30","volume-title":"ICFEM","author":"Y. Yang","year":"2004","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schutte, W., Barnett, M. (eds.) ICFEM. LNCS, vol.\u00a03308, pp.\u00a030\u201345 (2004)"},{"key":"18_CR81","first-page":"8:1","volume-title":"PADTAD","author":"J. Yi","year":"2009","unstructured":"Yi, J., Sadowski, C., Flanagan, C.: SideTrack: generalizing dynamic atomicity analysis. In: PADTAD, pp.\u00a08:1\u20138:10. ACM, New York (2009)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:25:35Z","timestamp":1751646335000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":81,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_18","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}