{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:10:47Z","timestamp":1774987847915,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642120015","type":"print"},{"value":"9783642120022","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12002-2_27","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T20:20:25Z","timestamp":1267993225000},"page":"328-342","source":"Crossref","is-referenced-by-count":59,"title":["Trace-Based Symbolic Analysis for Atomicity Violations"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rhishikesh","family":"Limaye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malay","family":"Ganai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access interleaving invariants. In: Architectural Support for Programming Languages and Operating Systems, pp. 37\u201348 (2006)","DOI":"10.1145\/1168918.1168864"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-02658-4_21","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P.: Meta-analysis for atomicity violations under nested locking. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol.\u00a05643, pp. 248\u2013262. Springer, Heidelberg (2009)"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Programming Language Design and Implementation, pp. 338\u2013349 (2003)","DOI":"10.1145\/780822.781169"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11817963_30","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2006","unstructured":"Farzan, A., Madhusudan, P.: Causal atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 315\u2013328. Springer, Heidelberg (2006)"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Xu, M., Bod\u00edk, R., Hill, M.D.: A serializability violation detector for shared-memory server programs. In: Programming Language Design and Implementation, pp. 1\u201314 (2005)","DOI":"10.1145\/1064978.1065013"},{"issue":"2","key":"27_CR6","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L. Wang","year":"2006","unstructured":"Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng.\u00a032(2), 93\u2013110 (2006)","journal-title":"IEEE Trans. Software Eng."},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-70545-1_8","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2008","unstructured":"Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 52\u201365. Springer, Heidelberg (2008)"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: PLDI, pp. 293\u2013303 (2008)","DOI":"10.1145\/1379022.1375618"},{"key":"27_CR9","volume-title":"Parallel and Distributed Processing Symposium (IPDPS)","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: Parallel and Distributed Processing Symposium (IPDPS). IEEE, Los Alamitos (2004)"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-3-642-00768-2_14","volume-title":"TACAS 2009","author":"A. Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P.: The complexity of predicting atomicity violations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 155\u2013169. Springer, Heidelberg (2009)"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-73368-3_27","volume-title":"Computer Aided Verification","author":"F. Chen","year":"2007","unstructured":"Chen, F., Rosu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 240\u2013253. Springer, Heidelberg (2007)"},{"key":"27_CR12","unstructured":"Serb\u0103nut\u0103, T.F., Chen, F., Rosu, G.: Maximal causal models for multithreaded systems. Technical Report UIUCDCS-R-2008-3017, University of Illinois at Urbana-Champaign (2008)"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-00590-9_28","volume-title":"Programming Languages and Systems","author":"C. Sadowski","year":"2009","unstructured":"Sadowski, C., Freund, S.N., Flanagan, C.: Singletrack: A dynamic determinism checker for multithreaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 394\u2013409. Springer, Heidelberg (2009)"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for dpll(t). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"27_CR16","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. Lahiri","year":"2009","unstructured":"Lahiri, S., Qadeer, S., Rakamaric, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol.\u00a05643, pp. 509\u2013524. Springer, Heidelberg (2009)"},{"key":"27_CR17","first-page":"23","volume-title":"Foundations of Software Engineering","author":"C. Wang","year":"2009","unstructured":"Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions. In: Foundations of Software Engineering, pp. 23\u201332. ACM, New York (2009)"},{"key":"27_CR18","first-page":"256","volume-title":"International Symposium on Formal Methods","author":"C. Wang","year":"2009","unstructured":"Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: International Symposium on Formal Methods, pp. 256\u2013272. ACM, New York (2009)"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivancic, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 505\u2013518. Springer, Heidelberg (2005)"},{"key":"27_CR20","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-78800-3_29","volume-title":"Tools and Algorithms for Construction and Analysis of Systems","author":"C. Wang","year":"2008","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 382\u2013396. Springer, Heidelberg (2008)"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Lee, J., Padua, D., Midkiff, S.: Basic compiler algorithms for parallel programs. In: Principles and Practice of Parallel Programming, pp. 1\u201312 (1999)","DOI":"10.1145\/329366.301105"},{"key":"27_CR22","first-page":"235","volume-title":"Design Automation Conference","author":"C. Wang","year":"2006","unstructured":"Wang, C., Gupta, A., Ganai, M.: Predicate learning and selective theory deduction for a difference logic solver. In: Design Automation Conference, pp. 235\u2013240. ACM, New York (2006)"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of c programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"27_CR24","unstructured":"Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: Parallel and Distributed Processing Symposium, p. 286 (2003)"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-70545-1_7","volume-title":"Computer Aided Verification","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 2008. LNCS, vol.\u00a05123, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"27_CR27","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1250734.1250737","volume-title":"PLDI","author":"S. Burckhardt","year":"2007","unstructured":"Burckhardt, S., Alur, R., Martin, M.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12\u201321. ACM, New York (2007)"},{"issue":"2","key":"27_CR28","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-004-0178-1","volume":"7","author":"T. Jussila","year":"2005","unstructured":"Jussila, T., Heljanlo, K., Niemel\u00e4, I.: BMC via on-the-fly determinization. STTT\u00a07(2), 89\u2013101 (2005)","journal-title":"STTT"},{"key":"27_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1390630.1390634","volume-title":"International Symposium on Software Testing and Analysis","author":"N. Beckman","year":"2008","unstructured":"Beckman, N., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: International Symposium on Software Testing and Analysis, pp. 3\u201314. ACM, New York (2008)"}],"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-642-12002-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:31:56Z","timestamp":1558272716000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12002-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120015","9783642120022"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12002-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}