Counterexample Guided Inductive Synthesis Modulo Theories

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

doi:10.1007/978-3-319-96145-3_15

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 proceeding › Conference Contribution (Conference Proceeding)

52 Citations (Scopus)

184 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 language	English
Title of host publication	Computer Aided Verification
Editors	Hana Chockler, Georg Weissenbacher
Publisher	Springer Nature
Pages	270-288
Number of pages	19
ISBN (Electronic)	978-3-319-96145-3
ISBN (Print)	978-3-319-96144-6
DOIs	https://doi.org/10.1007/978-3-319-96145-3_15
Publication status	Published - 18 Jul 2018
Event	International Conference on Computer Aided Verification - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018 Conference number: 30 http://cavconference.org/2018/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Nature
Volume	10981
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Computer Aided Verification
Abbreviated title	CAV 2018
Country/Territory	United Kingdom
City	Oxford
Period	14/07/18 → 17/07/18
Internet address	http://cavconference.org/2018/

Research Groups and Themes

Programming Languages

Access to Document

10.1007/978-3-319-96145-3_15

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via Springer Nature at https://link.springer.com/chapter/10.1007/978-3-319-96145-3_15. Please refer to any applicable terms of use of the publisher.
Final published version, 607 KBLicence: CC BY

Handle.net

Persistent link

Embargoed Document

Full-text PDF (accepted author manuscript)
Accepted author manuscript, 394 KB

Dr Cristina David
- cristina.davidbristol.acuk
- School of Computer Science - Senior Lecturer
Person: Academic

Cite this

@inproceedings{1f6397ed548444b9b5cce26c603da4d9,

title = "Counterexample Guided Inductive Synthesis Modulo Theories",

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.",

author = "Alessandro Abate and Cristina David and Pascal Kesseli and Daniel Kroening and Elizabeth Polgreen",

year = "2018",

month = jul,

day = "18",

doi = "10.1007/978-3-319-96145-3\_15",

language = "English",

isbn = "978-3-319-96144-6",

series = "Lecture Notes in Computer Science ",

publisher = "Springer Nature",

pages = "270--288",

editor = "Hana Chockler and Georg Weissenbacher",

booktitle = "Computer Aided Verification",

address = "United Kingdom",

note = "International Conference on Computer Aided Verification, CAV 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

url = "http://cavconference.org/2018/",

}

Abate, A, David, C, Kesseli, P, Kroening, D & Polgreen, E 2018, Counterexample Guided Inductive Synthesis Modulo Theories. in H Chockler & G Weissenbacher (eds), Computer Aided Verification. Lecture Notes in Computer Science , vol. 10981, Springer Nature, pp. 270-288, International Conference on Computer Aided Verification, Oxford, United Kingdom, 14/07/18. https://doi.org/10.1007/978-3-319-96145-3_15

Counterexample Guided Inductive Synthesis Modulo Theories. / Abate, Alessandro ; David, Cristina; Kesseli, Pascal et al.
Computer Aided Verification. ed. / Hana Chockler; Georg Weissenbacher. Springer Nature, 2018. p. 270-288 (Lecture Notes in Computer Science ; Vol. 10981).

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

TY - GEN

T1 - Counterexample Guided Inductive Synthesis Modulo Theories

AU - Abate, Alessandro

AU - David, Cristina

AU - Kesseli, Pascal

AU - Kroening, Daniel

AU - Polgreen, Elizabeth

N1 - Conference code: 30

PY - 2018/7/18

Y1 - 2018/7/18

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-96145-3_15

DO - 10.1007/978-3-319-96145-3_15

M3 - Conference Contribution (Conference Proceeding)

SN - 978-3-319-96144-6

T3 - Lecture Notes in Computer Science

SP - 270

EP - 288

BT - Computer Aided Verification

A2 - Chockler, Hana

A2 - Weissenbacher, Georg

PB - Springer Nature

T2 - International Conference on Computer Aided Verification

Y2 - 14 July 2018 through 17 July 2018

ER -

Counterexample Guided Inductive Synthesis Modulo Theories

Abstract

Publication series

Conference

Research Groups and Themes

Access to Document

Handle.net

Embargoed Document

Fingerprint

Profiles

Dr Cristina David

Cite this