{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T01:55:31Z","timestamp":1772243731808,"version":"3.50.1"},"reference-count":0,"publisher":"IOS Press","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:p>The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. Our goal is to identify the core computational problem common to these proposals in a logical framework. The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. We describe alternative solution strategies that combine learning, counterexample analysis and constraint solving. We report on prototype implementations, and present experimental results on the set of benchmarks collected as part of the first SyGuS-Comp competition held in July 2014.<\/jats:p>","DOI":"10.3233\/978-1-61499-495-4-1","type":"book-chapter","created":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T14:11:46Z","timestamp":1739974306000},"source":"Crossref","is-referenced-by-count":9,"title":["Syntax-Guided Synthesis"],"prefix":"10.3233","author":[{"family":"Alur Rajeev","sequence":"additional","affiliation":[]},{"family":"Bodik Rastislav","sequence":"additional","affiliation":[]},{"family":"Dallal Eric","sequence":"additional","affiliation":[]},{"family":"Fisman Dana","sequence":"additional","affiliation":[]},{"family":"Garg Pranav","sequence":"additional","affiliation":[]},{"family":"Juniwal Garvit","sequence":"additional","affiliation":[]},{"family":"Kress-Gazit Hadas","sequence":"additional","affiliation":[]},{"family":"Madhusudan P.","sequence":"additional","affiliation":[]},{"family":"Martin Milo M.K.","sequence":"additional","affiliation":[]},{"family":"Raghothaman Mukund","sequence":"additional","affiliation":[]},{"family":"Saha Shamwaditya","sequence":"additional","affiliation":[]},{"family":"Seshia Sanjit A.","sequence":"additional","affiliation":[]},{"family":"Singh Rishabh","sequence":"additional","affiliation":[]},{"family":"Solar-Lezama Armando","sequence":"additional","affiliation":[]},{"family":"Torlak Emina","sequence":"additional","affiliation":[]},{"family":"Udupa Abhishek","sequence":"additional","affiliation":[]}],"member":"7437","container-title":["NATO Science for Peace and Security Series - D: Information and Communication Security","Dependable Software Systems Engineering"],"original-title":[],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T14:23:24Z","timestamp":1739975004000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospressISBN&isbn=978-1-61499-494-7&spage=1&doi=10.3233\/978-1-61499-495-4-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/978-1-61499-495-4-1","relation":{"is-cited-by":[{"id-type":"doi","id":"10.4204\/EPTCS.202.3","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-030-25540-4_5","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.229.13","asserted-by":"object"},{"id-type":"doi","id":"10.4204\/EPTCS.229.9","asserted-by":"object"},{"id-type":"doi","id":"10.1007\/978-3-030-78230-6_1","asserted-by":"object"},{"id-type":"doi","id":"10.1145\/3453483.3454104","asserted-by":"object"}]},"ISSN":["1874-6268"],"issn-type":[{"value":"1874-6268","type":"print"}],"subject":[],"published":{"date-parts":[[2015]]}}}