{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:15:20Z","timestamp":1763968520135,"version":"3.37.3"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T00:00:00Z","timestamp":1683936000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T00:00:00Z","timestamp":1683936000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"crossref","award":["UF160079"],"award-info":[{"award-number":["UF160079"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Research Council","award":["280053"],"award-info":[{"award-number":["280053"]}]},{"DOI":"10.13039\/100010664","name":"H2020 Future and Emerging Technologies","doi-asserted-by":"crossref","award":["712689"],"award-info":[{"award-number":["712689"]}],"id":[{"id":"10.13039\/100010664","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. While useful in general, such syntactic restrictions provide little help for the generation of programs that contain non-trivial constants, unless the user is able to provide the constants in advance. This is a fundamentally difficult task for state-of-the-art synthesisers. We propose a new approach to the synthesis of programs with non-trivial constants that combines the strengths of a counterexample-guided inductive synthesiser with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {T}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>T<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>), where <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {T}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>T<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is a first-order theory. We present two exemplars, one based on Fourier-Motzkin (FM) variable elimination and one based on first-order satisfiability. We demonstrate the practical value of CEGIS(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {T}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>T<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {T}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>T<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) within the mature synthesiser CVC4 and show that CEGIS(<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {T}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>T<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) improves CVC4\u2019s results.<\/jats:p>","DOI":"10.1007\/s10817-023-09664-4","type":"journal-article","created":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T11:56:36Z","timestamp":1684151796000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Synthesising Programs with Non-trivial Constants"],"prefix":"10.1007","volume":"67","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9106-934X","authenticated-orcid":false,"given":"Cristina","family":"David","sequence":"additional","affiliation":[]},{"given":"Pascal","family":"Kesseli","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Elizabeth","family":"Polgreen","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,5,13]]},"reference":[{"key":"9664_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: CAV (1), Lecture Notes in Computer Science, vol. 10981, pp. 270\u2013288. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"9664_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: CAV, LNCS, vol. 8044, pp. 934\u2013950. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"9664_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"9664_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Cern\u00fd, P., Radhakrishna, A.: Synthesis through unification. In: CAV, LNCS, vol. 9207, pp. 163\u2013179. Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_10"},{"key":"9664_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: SyGuS-Comp 2017: Results and analysis. CoRR abs\/1711.11438 (2017)","DOI":"10.4204\/EPTCS.260.9"},{"key":"9664_CR6","unstructured":"Alur, R., Fisman, D., Singh, R., Udupa, A.: Syntax guided synthesis competition. http:\/\/sygus.seas.upenn.edu\/SyGuS-COMP2017.html (2017)"},{"key":"9664_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: TACAS, LNCS, vol. 10205, pp. 319\u2013336 (2017)","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"9664_CR8","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Reynolds, A., Larraz, D., Tinelli, C.: Extending enumerative function synthesis via SMT-driven classification. In: Barrett, C.W., Yang, J. (eds.) Formal Methods In Computer-Aided Design (FMCAD), pp. 212\u2013220. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894267","DOI":"10.23919\/FMCAD.2019.8894267"},{"issue":"1\u20132","key":"9664_CR9","first-page":"21","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1\u20132), 21\u201346 (2007)","journal-title":"JSAT"},{"key":"9664_CR10","volume-title":"Implementation of Fourier-Motzkin elimination","author":"AJC Bik","year":"1994","unstructured":"Bik, A.J.C., Wijshoff, H.A.G.: Implementation of Fourier-Motzkin elimination. Rijksuniversiteit Leiden, Tech. rep. (1994)"},{"key":"9664_CR11","doi-asserted-by":"publisher","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Design Automation Conference, DAC \u201903, pp. 368\u2013371. ACM, New York, NY, USA (2003). https:\/\/doi.org\/10.1145\/775832.775928","DOI":"10.1145\/775832.775928"},{"key":"9664_CR12","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages, LNCS, vol.\u00a033, pp. 134\u2013183. Springer (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"9664_CR13","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: Principles of Programming Languages, POPL, pp. 238\u2013252 (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"9664_CR14","doi-asserted-by":"crossref","unstructured":"David, C., Kesseli, P., Kroening, D., Lewis, M.: Danger invariants. In: Formal Methods (FM), LNCS, vol. 9995, pp. 182\u2013198. Springer (2016)","DOI":"10.1007\/978-3-319-48989-6_12"},{"key":"9664_CR15","doi-asserted-by":"crossref","unstructured":"David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. In: LPAR, LNCS, vol. 9450, pp. 483\u2013498. Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_34"},{"key":"9664_CR16","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS, LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9664_CR17","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: SAT, LNCS, vol. 2919, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9664_CR18","doi-asserted-by":"crossref","unstructured":"Feng, Y., Bastani, O., Martins, R., Dillig, I., Anand, S.: Automated synthesis of semantic malware signatures using maximum satisfiability. In: NDSS. The Internet Society (2017)","DOI":"10.14722\/ndss.2017.23379"},{"key":"9664_CR19","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Geffen, J.V., Dillig, I., Chaudhuri, S.: Component-based synthesis of table consolidation and transformation tasks from examples. In: PLDI, pp. 422\u2013436. ACM (2017)","DOI":"10.1145\/3140587.3062351"},{"key":"9664_CR20","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: POPL, pp. 599\u2013612. ACM (2017)","DOI":"10.1145\/3093333.3009851"},{"key":"9664_CR21","doi-asserted-by":"publisher","unstructured":"Floyd, R.W.: Assigning Meanings to Programs, pp. 65\u201381. Springer, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"9664_CR22","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: CAV, LNCS, vol. 3114, pp. 175\u2013188. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"9664_CR23","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62\u201373. ACM (2011)","DOI":"10.1145\/1993316.1993506"},{"key":"9664_CR24","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: PLDI, pp. 50\u201361. ACM (2011)","DOI":"10.1145\/1993316.1993505"},{"issue":"1\u20132","key":"9664_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2500000010","volume":"4","author":"S Gulwani","year":"2017","unstructured":"Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends Program. Lang. 4(1\u20132), 1\u2013119 (2017). https:\/\/doi.org\/10.1561\/2500000010","journal-title":"Found. Trends Program. Lang."},{"key":"9664_CR26","doi-asserted-by":"publisher","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.: Proving non-termination. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 147\u2013158 (2008). https:\/\/doi.org\/10.1145\/1328438.1328459","DOI":"10.1145\/1328438.1328459"},{"key":"9664_CR27","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE (1), pp. 215\u2013224. ACM (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"9664_CR28","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer (2008)"},{"key":"9664_CR29","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. In: IJCAI, pp. 542\u2013551. William Kaufmann (1979)"},{"key":"9664_CR30","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification (CAV), Part II, Lecture Notes in Computer Science, vol. 10982, pp. 236\u2013255. Springer (2018)","DOI":"10.1007\/978-3-319-96142-2_16"},{"issue":"6","key":"9664_CR31","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9664_CR32","doi-asserted-by":"crossref","unstructured":"Perelman, D., Gulwani, S., Grossman, D., Provost, P.: Test-driven synthesis. In: PLDI, pp. 408\u2013418. ACM (2014)","DOI":"10.1145\/2666356.2594297"},{"key":"9664_CR33","unstructured":"Raghothaman, M., Udupa, A.: Language to specify syntax-guided synthesis problems. CoRR abs\/1405.5590 (2014)"},{"key":"9664_CR34","doi-asserted-by":"crossref","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.) Computer Aided Verification (CAV), Part II. Lecture Notes in Computer Science, vol. 11562, pp. 74\u201383. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"9664_CR35","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: CAV (2), LNCS, vol. 9207, pp. 198\u2013216. Springer (2015)","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"9664_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0290-y","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. (2017). https:\/\/doi.org\/10.1007\/s10703-017-0290-y","journal-title":"Formal Methods Syst. Des."},{"key":"9664_CR37","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.: Datatypes with shared selectors. In: D.\u00a0Galmiche, S.\u00a0Schulz, R.\u00a0Sebastiani (eds.) International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Computer Science, vol. 10900, pp. 591\u2013608. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_39"},{"issue":"4\u20135","key":"9664_CR38","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/s001530050126","volume":"38","author":"E Rosen","year":"1999","unstructured":"Rosen, E.: An existential fragment of second order logic. Arch. Math. Log. 38(4\u20135), 217\u2013234 (1999)","journal-title":"Arch. Math. Log."},{"key":"9664_CR39","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131\u2013153 (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-131","DOI":"10.3233\/978-1-58603-929-5-131"},{"issue":"5\u20136","key":"9664_CR40","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"key":"9664_CR41","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI, pp. 281\u2013294. ACM (2005)","DOI":"10.1145\/1064978.1065045"},{"key":"9664_CR42","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168918.1168907"},{"key":"9664_CR43","doi-asserted-by":"crossref","unstructured":"Strichman, O.: On solving Presburger and linear arithmetic with SAT. In: FMCAD, LNCS, vol. 2517, pp. 160\u2013170. Springer (2002)","DOI":"10.1007\/3-540-36126-X_10"},{"key":"9664_CR44","unstructured":"SyGuS: Syntax-guided synthesis competition. http:\/\/www.sygus.org\/. Accessed 14 Oct 2019"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09664-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09664-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09664-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,21]],"date-time":"2023-06-21T11:04:34Z","timestamp":1687345474000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09664-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,13]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["9664"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09664-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,5,13]]},"assertion":[{"value":"29 April 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 May 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"Cesare Tinelli, an author of this paper, is also on the journal\u2019s editorial board. All the other authors declare they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"19"}}