| Title: |
Counterexample Guided Inductive Synthesis Modulo Theories |
| Authors: |
Abate, Alessandro; David, Cristina; Kesseli, Pascal; Kroening, Daniel; Polgreen, Elizabeth |
| Publication Year: |
2019 |
| Collection: |
Apollo - University of Cambridge Repository |
| Description: |
Program synthesis is the mechanized 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. We propose a new approach to program synthesis that combines the strengths of a counterexample-guided inductive synthesizer with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T ), where T is a first-order theory. In this paper, we focus on one particular challenge for program synthesizers, namely the generation of programs that require non-trivial constants. This is a fundamentally difficult task for state-of-the-art synthesizers. 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(T ) by automatically synthesizing programs for a set of intricate benchmarks. ; Royal Society University Research Fellowship UF160079 |
| Document Type: |
conference object |
| File Description: |
application/pdf |
| Language: |
English |
| Relation: |
https://www.repository.cam.ac.uk/handle/1810/287744 |
| DOI: |
10.17863/CAM.35060 |
| Availability: |
https://www.repository.cam.ac.uk/handle/1810/287744; https://doi.org/10.17863/CAM.35060 |
| Accession Number: |
edsbas.DB8C0E2C |
| Database: |
BASE |