Repository logo
 

Counterexample Guided Inductive Synthesis Modulo Theories

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Abate, Alessandro 
David, Cristina 
Kesseli, Pascal 
Kroening, Daniel 
Polgreen, Elizabeth 

Abstract

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.

Description

Keywords

Journal Title

Conference Name

Computer Aided Verification

Journal ISSN

Volume Title

Publisher

Sponsorship
Royal Society (UF160079)
Royal Society University Research Fellowship UF160079