{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:47:59Z","timestamp":1740142079631,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T00:00:00Z","timestamp":1558137600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T00:00:00Z","timestamp":1558137600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"National Science Foundation","award":["1302524"],"award-info":[{"award-number":["1302524"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2019,9]]},"DOI":"10.1007\/s11334-019-00343-5","type":"journal-article","created":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T14:01:16Z","timestamp":1558188076000},"page":"289-306","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Model-checking task-parallel programs for data-race"],"prefix":"10.1007","volume":"15","author":[{"given":"Radha","family":"Nakade","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2264-2958","authenticated-orcid":false,"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0602-2000","authenticated-orcid":false,"given":"Peter","family":"Aldous","sequence":"additional","affiliation":[]},{"given":"Kyle","family":"Storey","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Ogles","sequence":"additional","affiliation":[]},{"given":"Joshua","family":"Hooker","sequence":"additional","affiliation":[]},{"given":"Sheridan Jacob","family":"Powell","sequence":"additional","affiliation":[]},{"given":"Jay","family":"McCarthy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,5,18]]},"reference":[{"issue":"1","key":"343_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2557833.2560582","volume":"39","author":"P Anderson","year":"2014","unstructured":"Anderson P, Chase B, Mercer E (2014) JPF verification of Habanero Java programs. ACM SIGSOFT Softw Eng Notes 39(1):1\u20137","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"343_CR2","doi-asserted-by":"crossref","unstructured":"Bender MA, Fineman JT, Gilbert S, Leiserson CE (2004) On-the-fly maintenance of series-parallel relationships in fork-join multithreaded programs. In: Proceedings of the sixteenth annual ACM symposium on parallelism in algorithms and architectures, SPAA \u201904. ACM, New York, NY, USA, pp 133\u2013144","DOI":"10.1145\/1007912.1007933"},{"issue":"OOPSLA","key":"343_CR3","doi-asserted-by":"publisher","first-page":"144:1","DOI":"10.1145\/3276514","volume":"2","author":"S Blackshear","year":"2018","unstructured":"Blackshear S, Gorogiannis N, Hearn PW, Sergey I (2018) RacerD: compositional static race detection. Proc ACM Program Lang 2(OOPSLA):144:1\u2013144:28","journal-title":"Proc ACM Program Lang"},{"issue":"1","key":"343_CR4","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1006\/jpdc.1996.0107","volume":"37","author":"RD Blumofe","year":"1996","unstructured":"Blumofe RD, Joerg CF, Kuszmaul BC, Leiserson CE, Randall KH, Zhou Y (1996) Cilk: an efficient multithreaded runtime system. J Parallel Distrib Comput 37(1):55\u201369","journal-title":"J Parallel Distrib Comput"},{"issue":"1","key":"343_CR5","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/2103621.2103681","volume":"47","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani A, Emmi M (2012) Analysis of recursively parallel programs. ACM SIGPLAN Not 47(1):203\u2013214","journal-title":"ACM SIGPLAN Not"},{"issue":"6","key":"343_CR6","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1002\/1096-9128(200005)12:6<375::AID-CPE480>3.0.CO;2-M","volume":"12","author":"JM Bull","year":"2000","unstructured":"Bull JM, Smith LA, Westhead MD, Henty DS, Davey RA (2000) A benchmark suite for high performance Java. Concurr\u2014Pract Exp 12(6):375\u2013388","journal-title":"Concurr\u2014Pract Exp"},{"key":"343_CR7","doi-asserted-by":"crossref","unstructured":"Cav\u00e9 V, Zhao J, Shirako J, Sarkar V (2011) Habanero-Java: the new adventures of old X10. In: Proceedings of the 9th international conference on principles and practice of programming in Java. ACM, pp 51\u201361","DOI":"10.1145\/2093157.2093165"},{"issue":"10","key":"343_CR8","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1145\/1103845.1094852","volume":"40","author":"P Charles","year":"2005","unstructured":"Charles P, Grothoff C, Saraswat V, Donawa C, Kielstra A, Ebcioglu K, von Praun C, Sarkar Vivek (2005) X10: an object-oriented approach to non-uniform cluster computing. SIGPLAN Not 40(10):519\u2013538","journal-title":"SIGPLAN Not"},{"key":"343_CR9","unstructured":"Cheng G-I, Feng M, Leiserson CE, Randall KH, Stark AF (1998) Detecting data races in Cilk programs that use locks. In: Proceedings of the tenth annual acm symposium on parallel algorithms and architectures, SPAA \u201998. ACM, New York, NY, USA, pp 298\u2013309"},{"issue":"5","key":"343_CR10","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/543552.512560","volume":"37","author":"J-D Choi","year":"2002","unstructured":"Choi J-D, Lee K, Loginov A, O\u2019Callahan R, Sarkar V, Sridharan M (2002) Efficient and precise datarace detection for multithreaded object-oriented programs. SIGPLAN Not 37(5):258\u2013269","journal-title":"SIGPLAN Not"},{"key":"343_CR11","doi-asserted-by":"crossref","unstructured":"Dennis JB, Gao GR, Sarkar V (2012) Determinacy and repeatability of parallel program schemata. In: Data-flow execution models for extreme scale computing (DFM), 2012, IEEE. IEEE, pp 1\u20139","DOI":"10.1109\/DFM.2012.10"},{"key":"343_CR12","doi-asserted-by":"crossref","unstructured":"Dimitrov D, Raychev V, Vechev M, Koskinen E (2014) Commutativity race detection. In: ACM SIGPLAN notices, vol 49:6. ACM, pp 305\u2013315","DOI":"10.1145\/2666356.2594322"},{"key":"343_CR13","doi-asserted-by":"crossref","unstructured":"Elmas T, Qadeer S, Tasiran S (2007) Goldilocks: a race and transaction-aware Java runtime. In: ACM SIGPLAN notices, vol 42:6. ACM, pp 245\u2013255","DOI":"10.1145\/1273442.1250762"},{"key":"343_CR14","doi-asserted-by":"crossref","unstructured":"Engler D, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. In: ACM SIGOPS operating systems review, vol 37:5. ACM, pp 237\u2013252","DOI":"10.1145\/1165389.945468"},{"key":"343_CR15","doi-asserted-by":"crossref","unstructured":"Feng M, Leiserson CE (1997) Efficient detection of determinacy races in Cilk programs. In: Proceedings of the ninth annual acm symposium on parallel algorithms and architectures, SPAA \u201997. ACM, New York, NY, USA, pp 1\u201311","DOI":"10.1145\/258492.258493"},{"key":"343_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan C, Freund SN (2009) FastTrack: efficient and precise dynamic race detection. In: ACM sigplan notices, vol. 44:6. ACM, pp 121\u2013133","DOI":"10.1145\/1543135.1542490"},{"key":"343_CR17","doi-asserted-by":"crossref","unstructured":"Gligoric M, Mehlitz PC, Marinov D (2012) X10X: model checking a new programming language with an \u201cold\u201d model checker. In: 2012 IEEE fifth international conference on software testing, verification and validation (ICST), IEEE. IEEE, pp 11\u201320","DOI":"10.1109\/ICST.2012.81"},{"key":"343_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid P (1997) Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL \u201997. ACM, New York, NY, USA, pp 174\u2013186","DOI":"10.1145\/263699.263717"},{"key":"343_CR19","doi-asserted-by":"crossref","unstructured":"Gotsman A, Berdine J, Cook B, Sagiv M (2007) Thread-modular shape analysis. In: ACM SIGPLAN notices, vol 42:6. ACM, pp 266\u2013277","DOI":"10.1145\/1273442.1250765"},{"issue":"6","key":"343_CR20","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1145\/2666356.2594315","volume":"49","author":"J Huang","year":"2014","unstructured":"Huang J, Meredith PO, Rosu G (2014) Maximal sound predictive race detection with control flow abstraction. SIGPLAN Not 49(6):337\u2013348","journal-title":"SIGPLAN Not"},{"key":"343_CR21","doi-asserted-by":"crossref","unstructured":"Imam S, Sarkar V (2014) Habanero-Java library: a Java 8 framework for multicore programming. In: Proceedings of the 2014 international conference on principles and practices of programming on the Java platform: virtual machines, languages, and Tools. ACM, pp 75\u201386","DOI":"10.1145\/2647508.2647514"},{"key":"343_CR22","unstructured":"Ji W (2013) TARDIS: task-level access race detection by intersecting sets"},{"key":"343_CR23","doi-asserted-by":"crossref","unstructured":"Kahlon V, Sinha N, Kruus E, Zhang Y (2009) Static data race detection for concurrent programs with asynchronous calls. In: Proceedings of the 7th joint meeting of the European software engineering conference and the foundations of software engineering. ACM, pp 13\u201322","DOI":"10.1145\/1595696.1595701"},{"issue":"6","key":"343_CR24","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/3140587.3062374","volume":"52","author":"D Kini","year":"2017","unstructured":"Kini D, Mathur U, Viswanathan M (2017) Dynamic race prediction in linear time. SIGPLAN Not 52(6):157\u2013170","journal-title":"SIGPLAN Not"},{"key":"343_CR25","doi-asserted-by":"crossref","unstructured":"Kini D, Mathur U, Viswanathan M (2018) Data race detection on compressed traces. In: Proceedings of the 2018 26th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering, ESEC\/FSE 2018. ACM, New York, NY, USA, pp 26\u201337","DOI":"10.1145\/3236024.3236025"},{"key":"343_CR26","unstructured":"Kulikov S, Shafiei N, Van Breugel F, Visser W (2010) Detecting data races with Java Pathfinder"},{"issue":"7","key":"343_CR27","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport L (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21(7):558\u2013565","journal-title":"Commun ACM"},{"issue":"6","key":"343_CR28","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1145\/2666356.2594300","volume":"49","author":"L Li","year":"2014","unstructured":"Li L, Ji W, Scott ML (2014) Dynamic enforcement of determinism in a parallel scripting language. SIGPLAN Not 49(6):519\u2013529","journal-title":"SIGPLAN Not"},{"key":"343_CR29","doi-asserted-by":"crossref","unstructured":"Malkis A, Podelski A, Rybalchenko A (2007) Precise thread-modular verification. In: Nielson HR, Fil\u00e9 G (eds) Static analysis. SAS 2007. Lecture notes in computer science, vol 4634. Springer, Berlin, Heidelberg, pp 218\u2013232","DOI":"10.1007\/978-3-540-74061-2_14"},{"key":"343_CR30","doi-asserted-by":"crossref","unstructured":"Mellor-Crummey J (1991) On-the-fly detection of data races for programs with nested fork-join parallelism. In: Proceedings of the 1991 ACM\/IEEE conference on supercomputing, supercomputing \u201991. ACM, New York, NY, USA, pp 24\u201333","DOI":"10.1145\/125826.125861"},{"key":"343_CR31","doi-asserted-by":"crossref","unstructured":"Mercer E, Anderson P, Vrvilo N, Sarkar V (2015) Model checking task parallel programs using gradual permissions. In: Proceedings of 30th IEEE\/ACM international conference on automated software engineering, new ideas category. ACM, pp. 535\u2013540","DOI":"10.1109\/ASE.2015.75"},{"key":"343_CR32","doi-asserted-by":"crossref","unstructured":"Raman R, Zhao J, Sarkar V, Vechev M, Yahav E (2012) Scalable and Precise dynamic datarace detection for structured parallelism. In: ACM SIGPLAN notices, vol 47:6. ACM, pp 531\u2013542","DOI":"10.1145\/2345156.2254127"},{"issue":"3","key":"343_CR33","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s10703-012-0143-7","volume":"41","author":"R Raman","year":"2012","unstructured":"Raman R, Zhao J, Sarkar V, Vechev MT, Yahav E (2012) Efficient data race detection for async-finish parallelism. Form Methods Syst Des 41(3):321\u2013347","journal-title":"Form Methods Syst Des"},{"key":"343_CR34","doi-asserted-by":"crossref","unstructured":"Surendran R, Sarkar V (2016) Dynamic determinacy race detection for task parallelism with futures. In: 2016 16th international conference on runtime verification. Springer, Sprinter, pp 1\u20132","DOI":"10.1007\/978-3-319-46982-9_23"},{"key":"343_CR35","doi-asserted-by":"crossref","unstructured":"Surendran R, Sarkar V (2016) Dynamic determinacy race detection for task parallelism with futures. Springer International Publishing, Cham, pp 368\u2013385","DOI":"10.1007\/978-3-319-46982-9_23"},{"key":"343_CR36","doi-asserted-by":"crossref","unstructured":"Utterback R, Agrawal K, Fineman JT, Lee I-T Angelina (2016) Provably good and practically efficient parallel race detection for fork-join programs. In: Proceedings of the 28th ACM symposium on parallelism in algorithms and architectures, SPAA \u201916. ACM, New York, NY, USA, pp 83\u201394","DOI":"10.1145\/2935764.2935801"},{"key":"343_CR37","unstructured":"Vechev M, Yahav E, Raman R, Sarkar V (2011) Automatic verification of determinism for structured parallel programs. In: Cousot R, Martel M (eds) Static analysis. SAS 2010. Lecture notes in computer science, vol 6337. Springer, Berlin, Heidelberg, pp 455\u2013471"},{"key":"343_CR38","doi-asserted-by":"crossref","unstructured":"Virouleau P, Brunet P, Broquedis F, Furmento N, Thibault S, Aumage O, Gautier T (2014) Evaluation of OpenMP dependent tasks with the KASTORS benchmark suite. In: 10th international workshop on OpenMP, IWOMP2014, IWOMP2014. Springer, Salvador, Brazil, France, pp 16\u201329","DOI":"10.1007\/978-3-319-11454-5_2"},{"key":"343_CR39","doi-asserted-by":"crossref","unstructured":"Voung JW, Voung Rx, Lerner S (2007) RELAY: static race detection on millions of lines of code. In: Proceedings of the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering. ACM, pp 205\u2013214","DOI":"10.1145\/1287624.1287654"},{"key":"343_CR40","doi-asserted-by":"crossref","unstructured":"Westbrook E, Zhao J, Budimli\u0107 Z, Sarkar V (2012) Practical permissions for race-free parallelism. In: ECOOP 2012\u2013object-oriented programming. Springer, pp 614\u2013639","DOI":"10.1007\/978-3-642-31057-7_27"},{"issue":"1","key":"343_CR41","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1145\/3200691.3178514","volume":"53","author":"JR Wilcox","year":"2018","unstructured":"Wilcox JR, Flanagan C, Freund SN (2018) VerifiedFT: a verified, high-performance precise dynamic race detector. SIGPLAN Not 53(1):354\u2013367","journal-title":"SIGPLAN Not"},{"key":"343_CR42","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-38088-4_14","volume":"7871","author":"TK Zirkel","year":"2013","unstructured":"Zirkel TK, Siegel SF, McClory T (2013) Automated verification of chapel programs using model checking and symbolic execution. NASA Form Methods 7871:198\u2013212","journal-title":"NASA Form Methods"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00343-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-019-00343-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-019-00343-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,16]],"date-time":"2020-05-16T23:23:56Z","timestamp":1589671436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-019-00343-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,18]]},"references-count":42,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["343"],"URL":"https:\/\/doi.org\/10.1007\/s11334-019-00343-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2019,5,18]]},"assertion":[{"value":"3 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 May 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 May 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}