Counterexample Guided Inductive Synthesis Modulo Theories

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

29 Downloads (Pure)

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(
T
T
), where
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(
T
T
) by automatically synthesizing programs for a set of intricate benchmarks.
Original languageEnglish
Title of host publicationComputer Aided Verification
EditorsHana Chockler, Georg Weissenbacher
PublisherSpringer Nature
Pages270-288
Number of pages19
ISBN (Electronic)978-3-319-96145-3
ISBN (Print)978-3-319-96144-6
DOIs
Publication statusPublished - 18 Jul 2018
EventInternational Conference on Computer Aided Verification - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018
Conference number: 30
http://cavconference.org/2018/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Nature
Volume10981
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Computer Aided Verification
Abbreviated titleCAV 2018
CountryUnited Kingdom
CityOxford
Period14/07/1817/07/18
Internet address

Structured keywords

  • Programming Languages

Fingerprint

Dive into the research topics of 'Counterexample Guided Inductive Synthesis Modulo Theories'. Together they form a unique fingerprint.

Cite this