{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:33Z","timestamp":1772164113902,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-15-2-0096"],"award-info":[{"award-number":["FA8750-15-2-0096"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1453386"],"award-info":[{"award-number":["1453386"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["307334"],"award-info":[{"award-number":["307334"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,6,11]]},"DOI":"10.1145\/3192366.3192395","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"120-134","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic reasoning for automatic signal placement"],"prefix":"10.1145","author":[{"given":"Kostas","family":"Ferles","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Jacob","family":"Van Geffen","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Yannis","family":"Smaragdakis","sequence":"additional","affiliation":[{"name":"University of Athens, Greece"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147403.1147413"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837628"},{"key":"e_1_3_2_2_3_1","volume-title":"Concurrent Programming: Principles and Practice","author":"Andrews Gregory R.","year":"1991","unstructured":"Gregory R. Andrews . 1991 . Concurrent Programming: Principles and Practice . Benjamin-Cummings Publishing Co., Inc. , Redwood City, CA, USA . Gregory R. Andrews. 1991. Concurrent Programming: Principles and Practice . Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, USA."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512975"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/583854.582440"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640108"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/214037.214100"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108970.1108975"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480917"},{"key":"e_1_3_2_2_10_1","volume-title":"Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach.","author":"\u010cern Pavol","year":"2013","unstructured":"Pavol \u010cern ` y, Thomas A Henzinger , Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. 2013 . Efficient synthesis for concurrency by semantics-preserving transformations. In International Conference on Computer Aided Verification . Springer , 951\u2013967. Pavol \u010cern`y, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. 2013. Efficient synthesis for concurrency by semantics-preserving transformations. In International Conference on Computer Aided Verification . Springer, 951\u2013967."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375619"},{"key":"e_1_3_2_2_12_1","volume-title":"Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems ( 2008 ), 337\u2013340. Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems (2008), 337\u2013340."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509539"},{"key":"e_1_3_2_2_14_1","volume-title":"The origin of concurrent programming","author":"Dijkstra Edsger W","unstructured":"Edsger W Dijkstra . 1971. Hierarchical ordering of sequential processes . In The origin of concurrent programming . Springer , 198\u2013227. Edsger W Dijkstra. 1971. Hierarchical ordering of sequential processes. In The origin of concurrent programming. Springer, 198\u2013227."},{"key":"e_1_3_2_2_15_1","volume-title":"Cooperating Sequential Processes","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra . 2002. Cooperating Sequential Processes . Springer New York , New York, NY , 65\u2013138. Edsger W. Dijkstra. 2002. Cooperating Sequential Processes . Springer New York, New York, NY, 65\u2013138."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_46"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509511"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0397-7"},{"key":"e_1_3_2_2_19_1","volume-title":"An Algorithmic Framework for Synthesis of Concurrent Programs","author":"Allen Emerson E","unstructured":"E Allen Emerson and Roopsha Samanta . 2011. An Algorithmic Framework for Synthesis of Concurrent Programs .. In ATVA. Springer , 522\u2013 530. E Allen Emerson and Roopsha Samanta. 2011. An Algorithmic Framework for Synthesis of Concurrent Programs.. In ATVA. Springer, 522\u2013 530."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190260"},{"key":"e_1_3_2_2_21_1","volume-title":"Isil Dillig, and Yannis Smaragdakis.","author":"Ferles Kostas","year":"2018","unstructured":"Kostas Ferles , Jacob Van Geffen , Isil Dillig, and Yannis Smaragdakis. 2018 . Symbolic Reasoning for Automatic Signal Placement (Extended Version) . (2018). arXiv: 1804.02503 Kostas Ferles, Jacob Van Geffen, Isil Dillig, and Yannis Smaragdakis. 2018. Symbolic Reasoning for Automatic Signal Placement (Extended Version). (2018). arXiv: 1804.02503"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786815"},{"key":"e_1_3_2_2_24_1","volume-title":"Operating system principles","author":"Hansen Per Brinch","unstructured":"Per Brinch Hansen . 1973. Operating system principles . Prentice-Hall, Inc. Per Brinch Hansen. 1973. Operating system principles. Prentice-Hall, Inc."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949340"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/165123.165164"},{"key":"e_1_3_2_2_27_1","volume-title":"Proceedings of the First ACM SIG-PLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing .","author":"Hicks Michael","year":"2006","unstructured":"Michael Hicks , Jeffrey S. Foster , and Polyvios Prattikakis . 2006 . Lock Inference for Atomic Sections . In Proceedings of the First ACM SIG-PLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing . Michael Hicks, Jeffrey S. Foster, and Polyvios Prattikakis. 2006. Lock Inference for Atomic Sections. In Proceedings of the First ACM SIG-PLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing ."},{"key":"e_1_3_2_2_28_1","unstructured":"C. A. R. Hoare. 1971. Towards a theory of parallel programming. In International Seminar on Operating System Techniques .  C. A. R. Hoare. 1971. Towards a theory of parallel programming. In International Seminar on Operating System Techniques ."},{"key":"e_1_3_2_2_29_1","volume-title":"Monitors: An operating system structuring concept. In The origin of concurrent programming","author":"Richard Hoare Charles Antony","year":"1974","unstructured":"Charles Antony Richard Hoare . 1974 . Monitors: An operating system structuring concept. In The origin of concurrent programming . Springer , 272\u2013294. Charles Antony Richard Hoare. 1974. Monitors: An operating system structuring concept. In The origin of concurrent programming. Springer, 272\u2013294."},{"key":"e_1_3_2_2_30_1","volume-title":"Proc. of PODC","volume":"4","author":"Hovemeyer David","year":"2004","unstructured":"David Hovemeyer and William Pugh . 2004 . Finding concurrency bugs in Java . In Proc. of PODC , Vol. 4 . David Hovemeyer and William Pugh. 2004. Finding concurrency bugs in Java. In Proc. of PODC, Vol. 4."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462175"},{"key":"e_1_3_2_2_32_1","first-page":"221","article-title":"Automated Concurrency-Bug Fixing","volume":"12","author":"Jin Guoliang","year":"2012","unstructured":"Guoliang Jin , Wei Zhang , Dongdong Deng , Ben Liblit , and Shan Lu . 2012 . Automated Concurrency-Bug Fixing .. In OSDI , Vol. 12. 221 \u2013 236 . Guoliang Jin, Wei Zhang, Dongdong Deng, Ben Liblit, and Shan Lu. 2012. Automated Concurrency-Bug Fixing.. In OSDI, Vol. 12. 221\u2013236.","journal-title":"OSDI"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_54"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882339"},{"key":"e_1_3_2_2_35_1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Kahlon Vineet","year":"2012","unstructured":"Vineet Kahlon . 2012. Automatic lock insertion in concurrent programs . In Formal Methods in Computer-Aided Design (FMCAD) , 2012 . IEEE , 16\u201323. Vineet Kahlon. 2012. Automatic lock insertion in concurrent programs. In Formal Methods in Computer-Aided Design (FMCAD), 2012. IEEE, 16\u201323."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.391"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771798"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_18"},{"key":"e_1_3_2_2_39_1","volume-title":"Larus and Ravi Rajwar","author":"James","year":"2007","unstructured":"James R. Larus and Ravi Rajwar . 2007 . Transactional Memory. Morgan & Claypool . James R. Larus and Ravi Rajwar. 2007. Transactional Memory. Morgan & Claypool."},{"key":"e_1_3_2_2_40_1","volume-title":"Concurrent Programming in Java","author":"Lea Doug","unstructured":"Doug Lea . 1999. Concurrent Programming in Java . Second Edition : Design Principles and Patterns (2nd ed.). Addison-Wesley . Doug Lea. 1999. Concurrent Programming in Java. Second Edition: Design Principles and Patterns (2nd ed.). Addison-Wesley."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1669112.1669181"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111068"},{"key":"e_1_3_2_2_43_1","first-page":"267","article-title":"Finding and Reproducing Heisenbugs in Concurrent Programs","volume":"8","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi , Shaz Qadeer , Thomas Ball , Gerard Basler , Piramanayagam Arumuga Nainar , and Iulian Neamtiu . 2008 . Finding and Reproducing Heisenbugs in Concurrent Programs .. In OSDI , Vol. 8. 267 \u2013 280 . Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs.. In OSDI, Vol. 8. 267\u2013280.","journal-title":"OSDI"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133255.1134018"},{"key":"e_1_3_2_2_45_1","unstructured":"Aleksey Shipilev Sergey Kuksenko Anders Astrand Staffan Freiberg and Henrik Loef. {n. d.}. OpenJDK: JMH. ({n. d.}). http:\/\/openjdk.java. net\/projects\/code-tools\/jmh\/  Aleksey Shipilev Sergey Kuksenko Anders Astrand Staffan Freiberg and Henrik Loef. {n. d.}. OpenJDK: JMH. ({n. d.}). http:\/\/openjdk.java. net\/projects\/code-tools\/jmh\/"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103702"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/781995.782008"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706338"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480913"},{"key":"e_1_3_2_2_50_1","first-page":"163","article-title":"Ad Hoc Synchronization Considered Harmful","volume":"10","author":"Xiong Weiwei","year":"2010","unstructured":"Weiwei Xiong , Soyeon Park , Jiaqi Zhang , Yuanyuan Zhou , and Zhiqiang Ma . 2010 . Ad Hoc Synchronization Considered Harmful .. In OSDI , Vol. 10. 163 \u2013 176 . Weiwei Xiong, Soyeon Park, Jiaqi Zhang, Yuanyuan Zhou, and Zhiqiang Ma. 2010. Ad Hoc Synchronization Considered Harmful.. In OSDI, Vol. 10. 163\u2013176.","journal-title":"OSDI"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_21"}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192395","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192395","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192395","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192395"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":51,"alternative-id":["10.1145\/3192366.3192395","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192395","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192395","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}