{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T18:00:13Z","timestamp":1725732013239},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642388552"},{"type":"electronic","value":"9783642388569"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_16","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T04:05:28Z","timestamp":1371269128000},"page":"283-303","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Synthesis of Deterministic Concurrency"],"prefix":"10.1007","author":[{"given":"Veselin","family":"Raychev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Agarwal, S., Barik, R., Sarkar, V., Shyamasundar, R.K.: May-happen-in-parallel analysis of x10 programs. In: PPoPP 2007: Proceedings of the 12th Symposium on Principles and Practice of Parallel Programming, pp. 183\u2013193. ACM (2007)","key":"16_CR1","DOI":"10.1145\/1229428.1229471"},{"unstructured":"Aviram, A., Weng, S.-C., Hu, S., Ford, B.: Efficient system-enforced deterministic parallelism. In: OSDI (2010)","key":"16_CR2"},{"doi-asserted-by":"crossref","unstructured":"Berger, E.D., Yang, T., Liu, T., Novark, G.: Grace: safe multithreaded programming for c\/c++. In: OOPSLA 2009 (2009)","key":"16_CR3","DOI":"10.1145\/1640089.1640096"},{"doi-asserted-by":"crossref","unstructured":"Blumofe, R.D., Joerg, C.F., Kuszmaul, B.C., Leiserson, C.E., Randall, K.H., Zhou, Y.: Cilk: an efficient multithreaded runtime system. In: PPoPP 1995 (1995)","key":"16_CR4","DOI":"10.1006\/jpdc.1996.0107"},{"doi-asserted-by":"crossref","unstructured":"Bocchino Jr., R.L., Adve, V.S., Dig, D., Adve, S.V., Heumann, S., Komuravelli, R., Overbey, J., Simmons, P., Sung, H., Vakilian, M.: A type and effect system for deterministic parallel java. In: OOPSLA 2009 (2009)","key":"16_CR5","DOI":"10.1145\/1640089.1640097"},{"doi-asserted-by":"crossref","unstructured":"Botincan, M., Dodds, M., Jagannathan, S.: Resource-sensitive synchronization inference by abduction. In: POPL 2012 (2012)","key":"16_CR6","DOI":"10.1145\/2103656.2103694"},{"doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Baldassin, A., Leijen, D.: Concurrent programming with revisions and isolation types. In: OOPSLA 2010 (2010)","key":"16_CR7","DOI":"10.1145\/1869459.1869515"},{"doi-asserted-by":"crossref","unstructured":"Cherem, S., Chilimbi, T., Gulwani, S.: Inferring locks for atomic sections. In: PLDI 2008 (2008)","key":"16_CR8","DOI":"10.1145\/1375581.1375619"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL 1997 (1977)","key":"16_CR9","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978 (1978)","key":"16_CR10","DOI":"10.1145\/512760.512770"},{"doi-asserted-by":"crossref","unstructured":"Devietti, J., Lucia, B., Ceze, L., Oskin, M.: Dmp: deterministic shared memory multiprocessing. In: ASPLOS 2009 (2009)","key":"16_CR11","DOI":"10.1145\/1508244.1508255"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: PPDP 2010 (2010)","key":"16_CR12","DOI":"10.1145\/1836089.1836091"},{"key":"16_CR13","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.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"unstructured":"Jin, G., Zhang, W., Deng, D., Liblit, B., Lu, S.: Automated concurrency-bug fixing. In: OSDI 2012 (2012)","key":"16_CR14"},{"doi-asserted-by":"crossref","unstructured":"Kawaguchi, M., Rondon, P., Bakst, A., Jhala, R.: Deterministic parallelism via liquid effects. In: PLDI 2012 (2012)","key":"16_CR15","DOI":"10.1145\/2254064.2254071"},{"unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD 2010 (2010)","key":"16_CR16"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-36579-6_12","volume-title":"Compiler Construction","author":"O. Lhot\u00e1k","year":"2003","unstructured":"Lhot\u00e1k, O., Hendren, L.: Scaling Java points-to analysis using SPARK. In: Hedin, G. (ed.) CC 2003. LNCS, vol.\u00a02622, pp. 153\u2013169. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: SIGOPS Oper. Syst. Rev. (2008)","key":"16_CR18","DOI":"10.1145\/1346281.1346323"},{"key":"16_CR19","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.\u00a05079, pp. 363\u2013377. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"McCloskey, B., Zhou, F., Gay, D., Brewer, E.: Autolocker: synchronization inference for atomic sections. In: POPL 2006 (2006)","key":"16_CR20","DOI":"10.1145\/1111037.1111068"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-19718-5_21","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2011","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded critical parallel c programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 398\u2013418. Springer, Heidelberg (2011)"},{"key":"16_CR22","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher Order Symbol. Comput.\u00a019, 31\u2013100 (2006)","journal-title":"Higher Order Symbol. Comput."},{"doi-asserted-by":"crossref","unstructured":"Navabi, A., Zhang, X., Jagannathan, S.: Quasi-static scheduling for safe futures. In: PPoPP 2008 (2008)","key":"16_CR23","DOI":"10.1145\/1345206.1345212"},{"doi-asserted-by":"crossref","unstructured":"Olszewski, M., Ansel, J., Amarasinghe, S.: Kendo: efficient deterministic multithreading in software. ASPLOS 2009 (2009)","key":"16_CR24","DOI":"10.1145\/1508244.1508256"},{"unstructured":"Habanero Multicore Software Research project, http:\/\/habanero.rice.edu\/hj","key":"16_CR25"},{"unstructured":"The SAT4J SAT solver, http:\/\/www.sat4j.org\/ .","key":"16_CR26"},{"unstructured":"Vall\u00e9e-Rai, R., et al.: Soot - a Java Optimization Framework. In: Proceedings of CASCON 1999, pp. 125\u2013135 (1999)","key":"16_CR27"},{"unstructured":"Vasudevan, N., Edwards, S.A.: A determinizing compiler. In: PLDI, FIT Session (2009)","key":"16_CR28"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-15769-1_28","volume-title":"Static Analysis","author":"M. Vechev","year":"2010","unstructured":"Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic verification of determinism for structured parallel programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 455\u2013471. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL 2010 (2010)","key":"16_CR30","DOI":"10.1145\/1706299.1706338"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,25]],"date-time":"2022-02-25T08:37:12Z","timestamp":1645778232000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}