{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:23:37Z","timestamp":1725899017970},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_20","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"227-242","source":"Crossref","is-referenced-by-count":5,"title":["Lock Removal for Concurrent Trace Programs"],"prefix":"10.1007","author":[{"given":"Vineet","family":"Kahlon","sequence":"first","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Aldrich, J., Chambers, C., Sirer, E.G., Eggers, S.J.: Static analyses for eliminating unnecessary synchronization from Java programs. In: International Symposium on Static Analysis, pp. 19\u201338 (1999)","DOI":"10.1007\/3-540-48294-6_2"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Bacon, D.F., Konuru, R.B., Murthy, C., Serrano, M.J.: Thin Locks: Featherweight synchronization for Java. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 258\u2013268 (1998)","DOI":"10.1145\/277652.277734"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Escape analysis for object-oriented languages: Application to Java. In: ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pp. 20\u201334 (1999)","DOI":"10.1145\/320385.320387"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bogda, J., H\u00f6lzle, U.: Removing unnecessary synchronization in Java. In: ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pp. 35\u201346 (1999)","DOI":"10.1145\/320385.320388"},{"key":"20_CR5","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., Ro\u015fu, G.: Parametric and Sliced Causality. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 240\u2013253. Springer, Heidelberg (2007)"},{"issue":"6","key":"20_CR6","doi-asserted-by":"publisher","first-page":"876","DOI":"10.1145\/945885.945892","volume":"25","author":"J.-D. Choi","year":"2003","unstructured":"Choi, J.-D., Gupta, M., Serrano, M.J., Sreedhar, V.C., Midkiff, S.P.: Stack allocation and synchronization optimizations for Java using escape analysis. ACM Trans. Program. Lang. Syst.\u00a025(6), 876\u2013910 (2003)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"20_CR7","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1006\/jpdc.1998.1441","volume":"49","author":"P.C. Diniz","year":"1998","unstructured":"Diniz, P.C., Rinard, M.C.: Lock coarsening: Eliminating lock overhead in automatically parallelized object-based programs. J. Parallel Distrib. Comput.\u00a049(2), 218\u2013244 (1998)","journal-title":"J. Parallel Distrib. Comput."},{"key":"20_CR8","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":"20_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P.: Complexity of pattern-based verification for multithreaded programs. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 499\u2013510 (2011)","DOI":"10.1145\/1925844.1926443"},{"key":"20_CR10","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":"20_CR11","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., Sorrentino, F.: Meta-analysis for Atomicity Violations under Nested Locking. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 248\u2013262. Springer, Heidelberg (2009)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: Parallel and Distributed Processing Symposium (2004)","DOI":"10.1145\/964001.964023"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-18275-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T.M. Gawlitza","year":"2011","unstructured":"Gawlitza, T.M., Lammich, P., M\u00fcller-Olm, M., Seidl, H., Wenner, A.: Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 199\u2013213. Springer, Heidelberg (2011)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. Springer (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Software Tools for Technology Transfer\u00a02(4) (2000)","DOI":"10.1007\/s100090050043"},{"key":"20_CR16","unstructured":"Joint cav\/issta special even on specification, verification, and testing of concurrent software, \n                    \n                      http:\/\/research.microsoft.com\/qadeer\/cavissta.htm"},{"key":"20_CR17","unstructured":"The java grande forum benchmark suite, \n                    \n                      http:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise cfl-reachability for threads communicating via locks. In: Symposium on Logic in Computer Science, pp. 27\u201336 (2009)","DOI":"10.1109\/LICS.2009.45"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-14295-6_39","volume-title":"Computer Aided Verification","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 2010. LNCS, vol.\u00a06174, pp. 434\u2013449. Springer, Heidelberg (2010)"},{"issue":"7","key":"20_CR20","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\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"20_CR21","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":"20_CR22","doi-asserted-by":"crossref","unstructured":"Ruf, E.: Effective synchronization removal for Java. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 208\u2013218 (2000)","DOI":"10.1145\/358438.349327"},{"key":"20_CR23","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)"},{"issue":"4","key":"20_CR24","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst.\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11494881_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Sen","year":"2005","unstructured":"Sen, K., Ro\u015fu, G., Agha, G.: Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol.\u00a03535, pp. 211\u2013226. Springer, Heidelberg (2005)"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: On interference abstractions. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 423\u2013434 (2011)","DOI":"10.1145\/1925844.1926433"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"von Praun, C., Gross, T.R.: Static detection of atomicity violations in object-oriented programs. Object Technology\u00a03(6) (2004)","DOI":"10.5381\/jot.2004.3.6.a5"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-05089-3_17","volume-title":"FM 2009: Formal Methods","author":"C. Wang","year":"2009","unstructured":"Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic Predictive Analysis for Concurrent Programs. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 256\u2013272. Springer, Heidelberg (2009)"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-12002-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-Based Symbolic Analysis for Atomicity Violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 328\u2013342. Springer, Heidelberg (2010)"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Zee, K., Rinard, M.C.: Write barrier removal by static analysis. In: ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pp. 191\u2013210 (2002)","DOI":"10.1145\/583854.582439"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:59:50Z","timestamp":1620129590000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}