{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:32:40Z","timestamp":1770280360026,"version":"3.49.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that providesa parser, a verifier, and enumerative SemGuS solvers. The paper also describes an initial set of SemGuS benchmarks, which form the basis for comparing SemGuS solvers, and presents an evaluation of the baseline enumerative solvers.\n<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_2","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"27-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The SemGuS Toolkit"],"prefix":"10.1007","author":[{"given":"Keith J. C.","family":"Johnson","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[]},{"given":"Loris","family":"D\u2019Antoni","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: 2013 Formal Methods in Computer-Aided Design, pp.\u00a01\u20138 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-662-54577-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2017","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part I. LNCS, vol. 10205, pp. 319\u2013336. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18"},{"key":"2_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Center for High Throughput Computing: Center for high throughput computing (2006). https:\/\/doi.org\/10.21231\/GNT1-HW21, https:\/\/chtc.cs.wisc.edu\/","DOI":"10.21231\/GNT1-HW21"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252. ACM (1977).https:\/\/doi.org\/10.1145\/512950.512973, https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"issue":"2 &3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2 &3), 103\u2013179 (1992)","journal-title":"J. Log. Program."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-030-81685-8_4","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2021","unstructured":"D\u2019Antoni, L., Hu, Q., Kim, J., Reps, T.: Programmable program synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 84\u2013109. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_4"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-030-25540-4_14","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 259\u2013277. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14"},{"key":"2_CR9","unstructured":"Gulwani, S.: Synthesis from examples. In: WAMBSE (Workshop on Advances in Model-Based Software Engineering) Special Issue, Infosys Labs Briefings. vol.\u00a010. Citeseer (2012)"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI \u201911, New York, NY, USA, pp. 62\u201373. Association for Computing Machinery (2011). https:\/\/doi.org\/10.1145\/1993498.1993506","DOI":"10.1145\/1993498.1993506"},{"issue":"1\u20132","key":"2_CR11","first-page":"1","volume":"4","author":"S Gulwani","year":"2017","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends\u00ae Program. Lang. 4(1\u20132), 1\u2013119 (2017)","journal-title":"Found. Trends\u00ae Program. Lang."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-96145-3_21","volume-title":"Computer Aided Verification","author":"Q Hu","year":"2018","unstructured":"Hu, Q., D\u2019Antoni, L.: Syntax-guided synthesis with quantitative syntactic objectives. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 386\u2013403. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_21"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Huang, K., Qiu, X., Shen, P., Wang, Y.: Reconciling enumerative and deductive program synthesis. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15\u201320, 2020, pp. 1159\u20131174. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3386027, https:\/\/doi.org\/10.1145\/3385412.3386027","DOI":"10.1145\/3385412.3386027"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering - Volume 1, ICSE 2010, Cape Town, South Africa, 1\u20138 May 2010, pp. 215\u2013224. ACM (2010). https:\/\/doi.org\/10.1145\/1806799.1806833","DOI":"10.1145\/1806799.1806833"},{"issue":"POPL","key":"2_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434311","volume":"5","author":"J Kim","year":"2021","unstructured":"Kim, J., Hu, Q., D\u2019Antoni, L., Reps, T.: Semantics-guided synthesis. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021)","journal-title":"Proc. ACM Program. Lang."},{"issue":"3","key":"2_CR16","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/3093335.2993244","volume":"52","author":"M Lee","year":"2016","unstructured":"Lee, M., So, S., Oh, H.: Synthesizing regular expressions from examples for introductory automata assignments. SIGPLAN Not. 52(3), 70\u201380 (2016). https:\/\/doi.org\/10.1145\/3093335.2993244","journal-title":"SIGPLAN Not."},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Li, X., Zhou, X., Dong, R., Zhang, Y., Wang, X.: Efficient bottom-up synthesis for programs with local variables. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632894","DOI":"10.1145\/3632894"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Miltner, A., Padhi, S., Millstein, T.D., Walker, D.: Data-driven inference of representation invariants. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15\u201320, 2020, pp. 1\u201315. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385967","DOI":"10.1145\/3385412.3385967"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-96142-2_16","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part II. LNCS, vol. 10982, pp. 236\u2013255. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-030-24258-9_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"A N\u00f6tzli","year":"2019","unstructured":"N\u00f6tzli, A., et al.: Syntax-guided rewrite rule enumeration for SMT solvers. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 279\u2013297. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_20"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Padhi, S., Polgreen, E., Raghothaman, M., Reynolds, A., Udupa, A.: The sygus language standard version 2.1. CoRR abs\/2312.06001 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2312.06001","DOI":"10.48550\/ARXIV.2312.06001"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-94583-1_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Polgreen","year":"2022","unstructured":"Polgreen, E., Reynolds, A., Seshia, S.A.: Satisfiability and\u00a0synthesis modulo oracles. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 263\u2013284. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_13"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Polozov, O., Gulwani, S.: FlashMeta: a framework for inductive program synthesis. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 107\u2013126 (2015)","DOI":"10.1145\/2814270.2814310"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-25543-5_5","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C., Tinelli, C.: cvc4sy: smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 74\u201383. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: EGG: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434304","DOI":"10.1145\/3434304"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:36Z","timestamp":1721891016000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}