{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:01Z","timestamp":1740098941402,"version":"3.37.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319667058"},{"type":"electronic","value":"9783319667065"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66706-5_13","type":"book-chapter","created":{"date-parts":[[2017,8,18]],"date-time":"2017-08-18T04:13:26Z","timestamp":1503029606000},"page":"253-276","source":"Crossref","is-referenced-by-count":8,"title":["Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs"],"prefix":"10.1007","author":[{"given":"Suvam","family":"Mukherjee","sequence":"first","affiliation":[]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[]},{"given":"Deepak","family":"D\u2019Souza","sequence":"additional","affiliation":[]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,19]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Artho, C., Havelund, K., Biere, A.: High-level data races. In: New Technologies for Information Systems, Proceedings of the 3rd International Workshop on New Developments in Digital Libraries, NDDL 2003, pp. 82\u201393 (2003)","DOI":"10.1002\/stvr.281"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_31"},{"key":"13_CR3","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. CoRR, abs\/cs\/0701193 (2007)"},{"key":"13_CR4","unstructured":"Carre, J.-L., Hymans, C.: From single-thread to multithreaded: an efficient static analysis algorithm. CoRR, abs\/0910.5833 (2009)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Chugh, R., Voung, J.W., Jhala, R., Lerner, A.: Dataflow analysis for concurrent programs using datarace detection. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7\u201313 June 2008, pp. 316\u2013326 (2008)","DOI":"10.1145\/1375581.1375620"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, Paris, France. Dunod (1976)","DOI":"10.1145\/390018.808314"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages, pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-19718-5_11","volume-title":"Programming Languages and Systems","author":"A De","year":"2011","unstructured":"De, A., D\u2019Souza, D., Nasre, R.: Dataflow analysis for datarace-free programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 196\u2013215. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19718-5_11"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Clarke, L.A.: Data flow analysis for verifying properties of concurrent programs. In: Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, SIGSOFT 1994, New Orleans, Louisiana, USA, 6\u20139 December 1994, pp. 62\u201375 (1994)","DOI":"10.1145\/193173.195295"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 297\u2013308 (2012)","DOI":"10.1145\/2103656.2103693"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 129\u2013142 (2013)","DOI":"10.1145\/2429069.2429086"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-11957-6_15","volume-title":"Programming Languages and Systems","author":"R Ferreira","year":"2010","unstructured":"Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267\u2013286. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11957-6_15"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp. 266\u2013277 (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Grunwald, D., Srinivasan, H.: Data flow equations for explicitly parallel programs. In: Proceedings of the Fourth ACM SIGPLAN Symposium on Principles & Practice of Parallel Programming (PPOPP), pp. 159\u2013168 (1993)","DOI":"10.1145\/155332.155349"},{"issue":"2","key":"13_CR16","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.entcs.2010.09.016","volume":"267","author":"B Jeannet","year":"2010","unstructured":"Jeannet, B.: Some experience on the software engineering of abstract interpretation tools. Electron. Notes Theor. Comput. Sci. 267(2), 29\u201342 (2010)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_52"},{"key":"13_CR18","unstructured":"Jones, C.B.: Developing methods for computer programs including a notion of interference. Ph.D. thesis, University of Oxford, UK (1981)"},{"key":"13_CR19","doi-asserted-by":"crossref","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, 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"13_CR20","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"9","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess progranm. IEEE Trans. Comput. 9, 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-69166-2_24","volume-title":"Static Analysis","author":"R Manevich","year":"2008","unstructured":"Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap decomposition for concurrent shape analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 363\u2013377. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-69166-2_24"},{"issue":"1","key":"13_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-8(1:26)2012","volume":"8","author":"A Min\u00e9","year":"2012","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Log. Methods Comput. Sci. 8(1), 1\u201363 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"13_CR23","unstructured":"Min\u00e9, A.: Static analysis by abstract interpretation of concurrent programs. Ph.D. thesis, Ecole Normale Sup\u00e9rieure de Paris-ENS Paris (2013)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-54013-4_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2014","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39\u201358. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54013-4_3"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-52234-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Monat","year":"2017","unstructured":"Monat, R., Min\u00e9, A.: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 386\u2013404. Springer, Cham (2017). doi: 10.1007\/978-3-319-52234-0_21"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Mukherjee, S., Padon, O., Shoham, S., D\u2019Souza, D., Rinetzky, N.: Thread-local semantics and its efficient sequential abstractions for race-free programs. http:\/\/www.csa.iisc.ernet.in\/TR\/2016\/3\/sasTechReport.pdf","DOI":"10.1007\/978-3-319-66706-5_13"},{"key":"13_CR27","unstructured":"Naik, M.: Chord: a program analysis platform for Java. http:\/\/www.cis.upenn.edu\/~mhnaik\/chord.html . Accessed 27 Mar 2017"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47764-0_1","volume-title":"Static Analysis","author":"M Rinard","year":"2001","unstructured":"Rinard, M.: Analysis of multithreaded programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 1\u201319. Springer, Heidelberg (2001). doi: 10.1007\/3-540-47764-0_1"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: a dynamic data race detector for multi-threaded programs. In: Proceedings of the Sixteenth ACM Symposium on Operating System Principles, SOSP, pp. 27\u201337 (1997)","DOI":"10.1145\/268998.266641"},{"key":"13_CR30","unstructured":"Vall\u00e9e-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot-a Java bytecode optimization framework. In: Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p. 13. IBM Press (1999)"},{"key":"13_CR31","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"X Qiwen","year":"1997","unstructured":"Qiwen, X., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Form. Asp. Comput. 9, 149\u2013174 (1997)","journal-title":"Form. Asp. Comput."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66706-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,25]],"date-time":"2023-08-25T03:53:05Z","timestamp":1692935585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66706-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319667058","9783319667065"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66706-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}