Skip to main content

Counterexample Guided Inductive Synthesis Modulo Theories

Alessandro Abate‚ Cristina David‚ Pascal Kesseli‚ Daniel Kroening and Elizabeth Polgreen

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. 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( \backslashmathcal \T T ), where \backslashmathcal \T 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( \backslashmathcal \T T ) by automatically synthesizing programs for a set of intricate benchmarks.

Address
Cham
Book Title
Computer Aided Verification
Editor
Chockler‚ Hana and Weissenbacher‚ Georg
ISBN
978−3−319−96145−3
Pages
270–288
Publisher
Springer International Publishing
Year
2018