Synthesizing imperative programs from examples guided by static analysis

Sunbeom So, Hakjoo Oh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

We present a novel algorithm for efficiently synthesizing imperative programs from examples. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our algorithm is based on enumerative synthesis, which explores all candidate programs in increasing size until it finds a solution. This algorithm, however, is too slow to be used in practice. Our key idea to accelerate the speed is to perform static analysis alongside the enumerative search, in order to “statically” identify and safely prune out partial programs that eventually fail to be a solution. We have implemented our algorithm in a tool, SIMPL, and evaluated it on 30 introductory programming problems gathered from online forums. The results show that our static analysis approach improves the speed of enumerative synthesis by 25x on average.

Original languageEnglish
Title of host publicationStatic Analysis - 24th International Symposium, SAS 2017, Proceedings
EditorsFrancesco Ranzato
PublisherSpringer Verlag
Pages364-381
Number of pages18
ISBN (Print)9783319667058
DOIs
Publication statusPublished - 2017 Jan 1
Event24th International Symposium on Static Analysis, SAS 2017 - New York, United States
Duration: 2017 Aug 302017 Sep 1

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10422 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Symposium on Static Analysis, SAS 2017
CountryUnited States
CityNew York
Period17/8/3017/9/1

Fingerprint

Static analysis
Static Analysis
Synthesis
Partial
Accelerate
Programming
Output

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

So, S., & Oh, H. (2017). Synthesizing imperative programs from examples guided by static analysis. In F. Ranzato (Ed.), Static Analysis - 24th International Symposium, SAS 2017, Proceedings (pp. 364-381). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10422 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-66706-5_18

Synthesizing imperative programs from examples guided by static analysis. / So, Sunbeom; Oh, Hakjoo.

Static Analysis - 24th International Symposium, SAS 2017, Proceedings. ed. / Francesco Ranzato. Springer Verlag, 2017. p. 364-381 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10422 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

So, S & Oh, H 2017, Synthesizing imperative programs from examples guided by static analysis. in F Ranzato (ed.), Static Analysis - 24th International Symposium, SAS 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10422 LNCS, Springer Verlag, pp. 364-381, 24th International Symposium on Static Analysis, SAS 2017, New York, United States, 17/8/30. https://doi.org/10.1007/978-3-319-66706-5_18
So S, Oh H. Synthesizing imperative programs from examples guided by static analysis. In Ranzato F, editor, Static Analysis - 24th International Symposium, SAS 2017, Proceedings. Springer Verlag. 2017. p. 364-381. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-66706-5_18
So, Sunbeom ; Oh, Hakjoo. / Synthesizing imperative programs from examples guided by static analysis. Static Analysis - 24th International Symposium, SAS 2017, Proceedings. editor / Francesco Ranzato. Springer Verlag, 2017. pp. 364-381 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{3f174bb541504f41843429c280ea04dd,
title = "Synthesizing imperative programs from examples guided by static analysis",
abstract = "We present a novel algorithm for efficiently synthesizing imperative programs from examples. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our algorithm is based on enumerative synthesis, which explores all candidate programs in increasing size until it finds a solution. This algorithm, however, is too slow to be used in practice. Our key idea to accelerate the speed is to perform static analysis alongside the enumerative search, in order to “statically” identify and safely prune out partial programs that eventually fail to be a solution. We have implemented our algorithm in a tool, SIMPL, and evaluated it on 30 introductory programming problems gathered from online forums. The results show that our static analysis approach improves the speed of enumerative synthesis by 25x on average.",
author = "Sunbeom So and Hakjoo Oh",
year = "2017",
month = "1",
day = "1",
doi = "10.1007/978-3-319-66706-5_18",
language = "English",
isbn = "9783319667058",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "364--381",
editor = "Francesco Ranzato",
booktitle = "Static Analysis - 24th International Symposium, SAS 2017, Proceedings",

}

TY - GEN

T1 - Synthesizing imperative programs from examples guided by static analysis

AU - So, Sunbeom

AU - Oh, Hakjoo

PY - 2017/1/1

Y1 - 2017/1/1

N2 - We present a novel algorithm for efficiently synthesizing imperative programs from examples. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our algorithm is based on enumerative synthesis, which explores all candidate programs in increasing size until it finds a solution. This algorithm, however, is too slow to be used in practice. Our key idea to accelerate the speed is to perform static analysis alongside the enumerative search, in order to “statically” identify and safely prune out partial programs that eventually fail to be a solution. We have implemented our algorithm in a tool, SIMPL, and evaluated it on 30 introductory programming problems gathered from online forums. The results show that our static analysis approach improves the speed of enumerative synthesis by 25x on average.

AB - We present a novel algorithm for efficiently synthesizing imperative programs from examples. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our algorithm is based on enumerative synthesis, which explores all candidate programs in increasing size until it finds a solution. This algorithm, however, is too slow to be used in practice. Our key idea to accelerate the speed is to perform static analysis alongside the enumerative search, in order to “statically” identify and safely prune out partial programs that eventually fail to be a solution. We have implemented our algorithm in a tool, SIMPL, and evaluated it on 30 introductory programming problems gathered from online forums. The results show that our static analysis approach improves the speed of enumerative synthesis by 25x on average.

UR - http://www.scopus.com/inward/record.url?scp=85028685445&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85028685445&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-66706-5_18

DO - 10.1007/978-3-319-66706-5_18

M3 - Conference contribution

AN - SCOPUS:85028685445

SN - 9783319667058

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 364

EP - 381

BT - Static Analysis - 24th International Symposium, SAS 2017, Proceedings

A2 - Ranzato, Francesco

PB - Springer Verlag

ER -