{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:05:58Z","timestamp":1759032358628,"version":"3.38.0"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2011,4,23]],"date-time":"2011-04-23T00:00:00Z","timestamp":1303516800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,11]]},"DOI":"10.1007\/s10009-011-0197-7","type":"journal-article","created":{"date-parts":[[2011,4,22]],"date-time":"2011-04-22T11:00:16Z","timestamp":1303470016000},"page":"495-518","source":"Crossref","is-referenced-by-count":9,"title":["Finding concurrency-related bugs using random isolation"],"prefix":"10.1007","volume":"13","author":[{"given":"Nicholas","family":"Kidd","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[]},{"given":"Julian","family":"Dolby","sequence":"additional","affiliation":[]},{"given":"Mandana","family":"Vaziri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,4,23]]},"reference":[{"issue":"4","key":"197_CR1","first-page":"397","volume":"77","author":"A. Ahmed","year":"2007","unstructured":"Ahmed A., Fluet M., Morrisett G.: L3: a linear language with locations. Fundam. Inf. 77(4), 397\u2013449 (2007)","journal-title":"Fundam. Inf."},{"key":"197_CR2","doi-asserted-by":"crossref","unstructured":"Aiken, A., Foster, J., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: PLDI. pp. 129\u2013140 (2003)","DOI":"10.1145\/780822.781146"},{"key":"197_CR3","doi-asserted-by":"crossref","unstructured":"Artho, C., Biere, A., Havelund, K.: Using block-local atomicity to detect stale-value concurrency errors. In: Proceedings of Second International Symposium on Automated Technology for Verification and Analysis (ATVA 2004), Taipei, Taiwan. LNCS, vol. 3299, pp. 150\u2013164. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30476-0_16"},{"issue":"4","key":"197_CR4","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1002\/stvr.281","volume":"13","author":"C. Artho","year":"2003","unstructured":"Artho C., Havelund K., Biere A.: High-level data races. J. Softw. Test. Verif. Reliab. (STVR) 13(4), 207\u2013227 (2003)","journal-title":"J. Softw. Test. Verif. Reliab. (STVR)"},{"key":"197_CR5","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: SAS, pp. 221\u2013239 (2006)","DOI":"10.1007\/11823230_15"},{"key":"197_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: SPIN, pp. 103\u2013122 (2001)","DOI":"10.1007\/3-540-45139-0_7"},{"key":"197_CR7","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: preventing data races and deadlocks. In OOPSLA, pp. 211\u2013230 (2002)","DOI":"10.1145\/583854.582440"},{"key":"197_CR8","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In LICS, pages 428\u2013239 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"issue":"12","key":"197_CR9","doi-asserted-by":"crossref","first-page":"1161","DOI":"10.1002\/cpe.866","volume":"16","author":"M. Burrows","year":"2004","unstructured":"Burrows M., Leino K.R.M.: Finding stale-value errors in concurrent programs. Conc. Comp. Prac. Exp. 16(12), 1161\u20131172 (2004)","journal-title":"Conc. Comp. Prac. Exp."},{"key":"197_CR10","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: TACAS, pp. 334\u2013349 (2006)","DOI":"10.1007\/11691372_22"},{"key":"197_CR11","doi-asserted-by":"crossref","unstructured":"Chase, D., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: PLDI, pp. 296\u2013310 (1990)","DOI":"10.1145\/93548.93585"},{"key":"197_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"197_CR13","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong versus weak updates. In: ESOP, pp. 246\u2013266 (2010)","DOI":"10.1007\/978-3-642-11957-6_14"},{"key":"197_CR14","doi-asserted-by":"crossref","unstructured":"Emmi, M., Jhala, R., Kohler, E., Majumdar, R.: Verifying reference counting implementations. In: TACAS, pp. 352\u2013367 (2009)","DOI":"10.1007\/978-3-642-00768-2_30"},{"issue":"3","key":"197_CR15","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1002\/cpe.1068","volume":"19","author":"Y. Eytani","year":"2007","unstructured":"Eytani Y., Havelund K., Stoller S.D., Ur S.: Towards a framework and a benchmark for testing tools for multi-threaded programs. Conc. Comp. Prac. Exp. 19(3), 267\u2013279 (2007)","journal-title":"Conc. Comp. Prac. Exp."},{"key":"197_CR16","doi-asserted-by":"crossref","unstructured":"Fahndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: PLDI, pp. 13\u201324 (2002)","DOI":"10.1145\/543552.512532"},{"key":"197_CR17","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. In: POPL, pp. 256\u2013267 (2004)","DOI":"10.1145\/982962.964023"},{"key":"197_CR18","doi-asserted-by":"crossref","unstructured":"Foster, J., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: PLDI, pp. 1\u201312 (2002)","DOI":"10.1145\/543552.512531"},{"key":"197_CR19","doi-asserted-by":"crossref","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T.W., Sagiv, S.: Numeric domains with summarized dimensions. In: TACAS, pp. 512\u2013529 (2004)","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"197_CR20","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: POPL, pp. 338\u2013350 (2005)","DOI":"10.1145\/1047659.1040333"},{"key":"197_CR21","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"197_CR22","doi-asserted-by":"crossref","unstructured":"Hammer, C., Dolby, J., Vaziri, M., Tip, F.: Dynamic detection of atomic-set serializability violations. In: ICSE, pp. 231\u2013240 (2008)","DOI":"10.1145\/1368088.1368120"},{"key":"197_CR23","doi-asserted-by":"crossref","unstructured":"Harris, W., Kidd, N., Chaki, S., Jha, S., Reps, T.: Verifying information flow control over unbounded processes. In: FM, pp. 773\u2013789 (2009)","DOI":"10.1007\/978-3-642-05089-3_49"},{"key":"197_CR24","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Pfeiffer, P., Reps, T.: Dependence analysis for pointer variables. In: PLDI, pp. 28\u201340 (1989)","DOI":"10.1145\/74818.74821"},{"key":"197_CR25","unstructured":"IBM: Watson Libraries for Analysis (WALA). http:\/\/wala.sourceforge.net\/wiki\/index.php (2009)"},{"key":"197_CR26","unstructured":"Jones, N., Muchnick, S.: Flow analysis and optimization of Lisp-like structures. In: Program Flow Analysis: Theory and Applications, pp. 66\u201374. Prentice-Hall, New Jersey (1981)"},{"key":"197_CR27","doi-asserted-by":"crossref","unstructured":"Jones, N., Muchnick, S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: POPL (1982)","DOI":"10.1145\/582153.582161"},{"key":"197_CR28","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta A.: On the analysis of interacting pushdown systems. In: POPL, pp. 303\u2013314 (2007)","DOI":"10.1145\/1190215.1190262"},{"key":"197_CR29","unstructured":"Kidd, N.: Static Verification of Data-Consistency Properties. PhD thesis, University of Wisconsin-Madison (2009)"},{"key":"197_CR30","doi-asserted-by":"crossref","unstructured":"Kidd, N., Lal, A., Reps, T.: Language strength reduction. In:SAS, pp. 283\u2013298 (2008)","DOI":"10.1007\/978-3-540-69166-2_19"},{"issue":"1","key":"197_CR31","doi-asserted-by":"crossref","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.: A decision procedure for detecting atomicity violations for communicating processes with locks. Int. J. Softw. Tools Tech. Transfer 13(1), 37\u201360 (2011)","journal-title":"Int. J. Softw. Tools Tech. Transfer"},{"key":"197_CR32","doi-asserted-by":"crossref","unstructured":"Kidd, N., Reps, T., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. In: VMCAI, pp. 198\u2013213 (2009a)","DOI":"10.1007\/978-3-540-93900-9_18"},{"key":"197_CR33","doi-asserted-by":"crossref","unstructured":"Kidd, N. A., Lammich, P., Touili, T., Reps, T.: A decision procedure for detecting atomicity violations for communicating processes with locks. In: SPIN, pp. 125\u2013142 (2009b)","DOI":"10.1007\/978-3-642-02652-2_12"},{"key":"197_CR34","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists, pp. 115\u2013126 (2006)","DOI":"10.1145\/1111320.1111048"},{"key":"197_CR35","doi-asserted-by":"crossref","unstructured":"Lammich, P., M\u00fcller-Olm, M.: Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In: SAS, pp. 205\u2013220 (2008)","DOI":"10.1007\/978-3-540-69166-2_14"},{"key":"197_CR36","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: SAS, pp. 280\u2013301 (2000)","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"197_CR37","doi-asserted-by":"crossref","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes\u2014a comprehensive study on real world concurrency bug characteristics. In: ASPLOS, pp. 329\u2013339 (2008)","DOI":"10.1145\/1353535.1346323"},{"key":"197_CR38","doi-asserted-by":"crossref","unstructured":"Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: Detecting atomicity violations via access-interleaving invariants. In: ASPLOS, pp. 37\u201348 (2006)","DOI":"10.1145\/1168918.1168864"},{"key":"197_CR39","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Verification of infinite state systems by compositional model checking. In: CHARME, pp. 219\u2013234 (1999)","DOI":"10.1007\/3-540-48153-2_17"},{"issue":"1","key":"197_CR40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1044834.1044835","volume":"14","author":"A. Milanova","year":"2005","unstructured":"Milanova A., Rountev A., Ryder B.G.: Parameterized object sensitivity for points-to analysis for Java. TOSEM 14(1), 1\u201341 (2005)","journal-title":"TOSEM"},{"key":"197_CR41","doi-asserted-by":"crossref","unstructured":"Min, S.L., Choi, J.-D.: An efficient cache-based access anomaly detection scheme. In: ASPLOS, pp. 235\u2013244 (1991)","DOI":"10.1145\/106974.106996"},{"key":"197_CR42","doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: POPL, pp. 327\u2013338 (2007)","DOI":"10.1145\/1190215.1190265"},{"key":"197_CR43","doi-asserted-by":"crossref","unstructured":"O\u2019Callahan, R., Choi, J.-D.: Hybrid dynamic data race detection. In: PPoPP, pp. 167\u2013178 (2003)","DOI":"10.1145\/966049.781528"},{"key":"197_CR44","doi-asserted-by":"crossref","unstructured":"Plevyak, J., Karamcheti, V., Chien, A.: Analysis of dynamic structures for efficient parallel execution. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) In: Workshop on Languages and Compilers for Parallel Computing, Portland, OR. Lecture Notes in Computer Science, vol. 768, pp. 37\u201357. Springer, Berlin (1993)","DOI":"10.1007\/3-540-57659-2_3"},{"key":"197_CR45","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, \u221e)-counter abstraction. In: CAV, pp. 107\u2013122 (2002)","DOI":"10.1007\/3-540-45657-0_9"},{"key":"197_CR46","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI, pp. 14\u201324 (2004)","DOI":"10.1145\/996893.996845"},{"key":"197_CR47","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22, 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"197_CR48","doi-asserted-by":"crossref","unstructured":"Rondon, P., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: POPL, pp. 131\u2013144 (2010)","DOI":"10.1145\/1707801.1706316"},{"issue":"1","key":"197_CR49","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv M., Reps T., Wilhelm R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst. 20(1), 1\u201350 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"197_CR50","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv M., Reps T., Wilhelm R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"197_CR51","doi-asserted-by":"crossref","unstructured":"Sasturkar, A., Agarwal, R., Wang, L., Stoller, S.D.: Automated type-based analysis of data races and atomicity. In: PPoPP, pp. 83\u201394 (2005)","DOI":"10.1145\/1065944.1065956"},{"issue":"4","key":"197_CR52","first-page":"391","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage S., Burrows M., Nelson G., Sobalvarro P., Anderson T.E.: Eraser: A dynamic data race detector for multithreaded programs. Theor. Comput. Sci. 15(4), 391\u2013411 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"197_CR53","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TUM (2002)"},{"key":"197_CR54","doi-asserted-by":"crossref","unstructured":"Vaziri, M., Tip, F., Dolby, J.: Associating synchronization constraints with data in an object-oriented language. In: POPL, pp. 334\u2013345 (2006)","DOI":"10.1145\/1111320.1111067"},{"key":"197_CR55","doi-asserted-by":"crossref","unstructured":"Walker, D., Morrisett, J.: Alias types for recursive data structures. In: Types in Compilation, pp. 177\u2013206 (2000)","DOI":"10.1007\/3-540-45332-6_7"},{"key":"197_CR56","doi-asserted-by":"crossref","unstructured":"Wang, L., Stoller, S.D.: Accurate and efficient runtime detection of atomicity errors in concurrent programs. In PPoPP, pp. 137\u2013146 (2006a)","DOI":"10.1145\/1122971.1122993"},{"key":"197_CR57","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L. Wang","year":"2006","unstructured":"Wang L., Stoller S.D.: Runtime analysis for atomicity of multithreaded programs. IEEE Trans. Softw. Eng. 32, 93\u2013110 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"197_CR58","doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci T., Bultan T.: Automated verification of concurrent linked lists with counters. In: SAS, pp. 69\u201384 (2002)","DOI":"10.1007\/3-540-45789-5_8"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0197-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0197-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0197-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T06:12:01Z","timestamp":1741155121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0197-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4,23]]},"references-count":58,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["197"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0197-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,4,23]]}}}