Synthesising Programs with Non-trivial Constants

“Synthesising Programs with Non-trivial Constants” by Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, and Cesare Tinelli. Journal of Automated Reasoning, vol. 67, no. 19, May 2023, Springer.

Abstract

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 costants, 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(\mathcalT), where \mathcalT 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(\mathcalT) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(\mathcalT) within the mature synthesiser CVC4 and show that CEGIS(\mathcalT) improves CVC4’s results.

Keywords: Program synthesis, Automated reasoning, Satisfiability modulo theories, Counterexample guided inductive synthesis

BibTeX entry:

@article{ABB+23,
   author = {Alessandro Abate and Haniel Barbosa and Clark Barrett and
	Cristina David and Pascal Kesseli and Daniel Kroening and
	Elizabeth Polgreen and Andrew Reynolds and Cesare Tinelli},
   title = {Synthesising Programs with Non-trivial Constants},
   journal = {Journal of Automated Reasoning},
   volume = {67},
   number = {19},
   publisher = {Springer},
   month = may,
   year = {2023},
   doi = {10.1007/s10817-023-09664-4},
   url = {http://theory.stanford.edu/~barrett/pubs/ABB+23.pdf}
}

(This webpage was created with bibtex2web.)