{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:05:42Z","timestamp":1767927942786,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523429","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"229-243","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Can reactive synthesis and syntax-guided synthesis be friends?"],"prefix":"10.1145","author":[{"given":"Wonhyuk","family":"Choi","sequence":"first","affiliation":[{"name":"Columbia University, USA"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[{"name":"CISPA, Germany"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"given":"Mark","family":"Santolucito","sequence":"additional","affiliation":[{"name":"Columbia University, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa.","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur , Rastislav Bodik , Garvit Juniwal , Milo MK Martin , Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013 . Syntax-guided synthesis. IEEE. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. IEEE."},{"key":"e_1_3_2_1_2_1","volume-title":"The 6th Competition on Syntax-Guided Synthesis. https:\/\/sygus.org\/comp\/2019\/results-slides.pdf Accessed: 2019-11-20","author":"Alur Rajeev","unstructured":"Rajeev Alur , Dana Fisman , Saswat Padhi , Andrew Reynolds , Rishabh Singh , and Abhishek Udupa . 2019. The 6th Competition on Syntax-Guided Synthesis. https:\/\/sygus.org\/comp\/2019\/results-slides.pdf Accessed: 2019-11-20 . Rajeev Alur, Dana Fisman, Saswat Padhi, Andrew Reynolds, Rishabh Singh, and Abhishek Udupa. 2019. The 6th Competition on Syntax-Guided Synthesis. https:\/\/sygus.org\/comp\/2019\/results-slides.pdf Accessed: 2019-11-20."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602999"},{"key":"e_1_3_2_1_5_1","volume-title":"Handbook of Model Checking","author":"Barrett Clark","unstructured":"Clark Barrett and Cesare Tinelli . 2018. Satisfiability modulo theories . In Handbook of Model Checking . Springer . Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. In Handbook of Model Checking. Springer."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Roderick Bloem Swen Jacobs and Ayrat Khalimov. 2014. Parameterized synthesis case study: AMBA AHB (extended version). arXiv preprint arXiv:1406.7608.  Roderick Bloem Swen Jacobs and Ayrat Khalimov. 2014. Parameterized synthesis case study: AMBA AHB (extended version). arXiv preprint arXiv:1406.7608.","DOI":"10.4204\/EPTCS.157.9"},{"key":"e_1_3_2_1_8_1","unstructured":"Benjamin Caulfield Markus N Rabe Sanjit A Seshia and Stavros Tripakis. 2015. What\u2019s Decidable about Syntax-Guided Synthesis? arXiv preprint arXiv:1510.08393.  Benjamin Caulfield Markus N Rabe Sanjit A Seshia and Stavros Tripakis. 2015. What\u2019s Decidable about Syntax-Guided Synthesis? arXiv preprint arXiv:1510.08393."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_11"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_38"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.229.3"},{"key":"e_1_3_2_1_12_1","volume-title":"Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications. In Asian Symposium on Programming Languages and Systems.","author":"Choi Wonhyuk","year":"2021","unstructured":"Wonhyuk Choi , Michel Vazirani , and Mark Santolucito . 2021 . Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications. In Asian Symposium on Programming Languages and Systems. Wonhyuk Choi, Michel Vazirani, and Mark Santolucito. 2021. Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications. In Asian Symposium on Programming Languages and Systems."},{"key":"e_1_3_2_1_13_1","volume-title":"Applications of recursive arithmetic to the problem of circuit synthesis. Summaries of the Summer Institute of Symbolic Logic at Cornell University","author":"Church Alonzo","unstructured":"Alonzo Church . 1957. Applications of recursive arithmetic to the problem of circuit synthesis. Summaries of the Summer Institute of Symbolic Logic at Cornell University , Vol. 1 . Alonzo Church. 1957. Applications of recursive arithmetic to the problem of circuit synthesis. Summaries of the Summer Institute of Symbolic Logic at Cornell University, Vol. 1."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_9"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258973"},{"key":"e_1_3_2_1_17_1","unstructured":"Bernd Finkbeiner Philippe Heim and Noemi Passing. 2021. Temporal Stream Logic modulo Theories. arxiv:2104.14988.  arxiv:2104.14988  Bernd Finkbeiner Philippe Heim and Noemi Passing. 2021. Temporal Stream Logic modulo Theories. arxiv:2104.14988.  arxiv:2104.14988"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342601"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_35"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani. 2011. Automating String Processing in Spreadsheets using Input-Output Examples. In POPL. https:\/\/www.microsoft.com\/en-us\/research\/publication\/automating-string-processing-spreadsheets-using-input-output-examples\/  Sumit Gulwani. 2011. Automating String Processing in Spreadsheets using Input-Output Examples. In POPL. https:\/\/www.microsoft.com\/en-us\/research\/publication\/automating-string-processing-spreadsheets-using-input-output-examples\/","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"e_1_3_2_1_22_1","volume-title":"An axiomatic basis for computer programming. Commun. ACM, 12, 10","author":"Richard Hoare Charles Antony","year":"1969","unstructured":"Charles Antony Richard Hoare . 1969. An axiomatic basis for computer programming. Commun. ACM, 12, 10 ( 1969 ). Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM, 12, 10 (1969)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178143"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_3_2_1_26_1","unstructured":"Swen Jacobs. 2014. Extended AIGER format for synthesis. arXiv preprint arXiv:1405.5793.  Swen Jacobs. 2014. Extended AIGER format for synthesis. arXiv preprint arXiv:1405.5793."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Swen Jacobs Felix Klein and Sebastian Schirmer. 2016. A high-level LTL synthesis format: TLSF v1. 1. arXiv preprint arXiv:1604.02284.  Swen Jacobs Felix Klein and Sebastian Schirmer. 2016. A high-level LTL synthesis format: TLSF v1. 1. arXiv preprint arXiv:1604.02284.","DOI":"10.4204\/EPTCS.229.10"},{"key":"e_1_3_2_1_28_1","volume-title":"The 7th Reactive Synthesis Competition","author":"Jacobs Swen","unstructured":"Swen Jacobs , Guillermo Perez , Roderick Bloem , and Armin Biere . 2020. The 7th Reactive Synthesis Competition . http:\/\/www.syntcomp.org\/wp-content\/uploads\/2020\/07\/SYNTCOMP2020-SYNT.pdf Accessed: 2021-05-18. Swen Jacobs, Guillermo Perez, Roderick Bloem, and Armin Biere. 2020. The 7th Reactive Synthesis Competition. http:\/\/www.syntcomp.org\/wp-content\/uploads\/2020\/07\/SYNTCOMP2020-SYNT.pdf Accessed: 2021-05-18."},{"key":"e_1_3_2_1_29_1","volume-title":"Specifying real-time properties with metric temporal logic. Real-time systems, 2, 4","author":"Koymans Ron","year":"1990","unstructured":"Ron Koymans . 1990. Specifying real-time properties with metric temporal logic. Real-time systems, 2, 4 ( 1990 ). Ron Koymans. 1990. Specifying real-time properties with metric temporal logic. Real-time systems, 2, 4 (1990)."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_40"},{"key":"e_1_3_2_1_31_1","unstructured":"Robert Love. 2010. Linux kernel development. Pearson Education.  Robert Love. 2010. Linux kernel development. Pearson Education."},{"key":"e_1_3_2_1_32_1","volume-title":"International Workshop\/20th Annual Conference of the EACSL.","author":"Madhusudan Parthasarathy","year":"2011","unstructured":"Parthasarathy Madhusudan . 2011 . Synthesizing reactive programs. In Computer Science Logic (CSL\u201911)-25th International Workshop\/20th Annual Conference of the EACSL. Parthasarathy Madhusudan. 2011. Synthesizing reactive programs. In Computer Science Logic (CSL\u201911)-25th International Workshop\/20th Annual Conference of the EACSL."},{"key":"e_1_3_2_1_33_1","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Maler Oded","unstructured":"Oded Maler and Dejan Nickovic . 2004. Monitoring temporal properties of continuous signals . In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems . Springer . Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035790"},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC \u201915)","author":"Raman Vasumathi","unstructured":"Vasumathi Raman , Alexandre Donz\u00e9 , Dorsa Sadigh , Richard M. Murray , and Sanjit A. Seshia . 2015. Reactive Synthesis from Signal Temporal Logic Specifications . In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC \u201915) . Association for Computing Machinery, New York, NY, USA. isbn:9781450334334 Vasumathi Raman, Alexandre Donz\u00e9, Dorsa Sadigh, Richard M. Murray, and Sanjit A. Seshia. 2015. Reactive Synthesis from Signal Temporal Logic Specifications. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC \u201915). Association for Computing Machinery, New York, NY, USA. isbn:9781450334334"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.229.8"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2019.00010"},{"key":"e_1_3_2_1_40_1","volume-title":"Peter Baer Galvin, and Greg Gagne","author":"Silberschatz Abraham","year":"2014","unstructured":"Abraham Silberschatz , Peter Baer Galvin, and Greg Gagne . 2014 . Operating system concepts essentials. Abraham Silberschatz, Peter Baer Galvin, and Greg Gagne. 2014. Operating system concepts essentials."}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523429","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523429","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:16Z","timestamp":1750188676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523429"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":39,"alternative-id":["10.1145\/3519939.3523429","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523429","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}