research-article

Synthesis of loop-free programs

Authors:

Ramarathnam VenkatesanAuthors Info & Claims

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 62 - 73

https://doi.org/10.1145/1993498.1993506

Published: 04 June 2011 Publication History

Abstract

We consider the problem of synthesizing loop-free programs that implement a desired functionality using components from a given library. Specifications of the desired functionality and the library components are provided as logical relations between their respective input and output variables. The library components can be used at most once, and hence the library is required to contain a reasonable overapproximation of the multiset of the components required.

We solve the above component-based synthesis problem using a constraint-based approach that involves first generating a synthesis constraint, and then solving the constraint. The synthesis constraint is a first-order ∃∀ logic formula whose size is quadratic in the number of components. We present a novel algorithm for solving such constraints. Our algorithm is based on counterexample guided iterative synthesis paradigm and uses off-the-shelf SMT solvers.

We present experimental results that show that our tool Brahma can efficiently synthesize highly nontrivial 10-20 line loop-free bitvector programs. These programs represent a state space of approximately 20¹⁰ programs, and are beyond the reach of the other tools based on sketching and superoptimization.

References

[1]

Satisfiability modulo theories competition (smt-comp). \URLhttp://www.smtcomp.org/2009/index.shtml.

[2]

SMTLIB: Satisfiability modulo theories lib. URLhttp://smtlib.org.

[3]

Yices: An SMT solver. URLhttp://yices.csl.sri.com.

[4]

The AHA! (A Hacker's Assistant) Superoptimizer, 2008. Download: URLhttp://www.hackersdelight.org/aha.zip, Documentation: URLhttp://www.hackersdelight.org/aha/aha.pdf.

[5]

S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In ASPLOS, 2006.

Digital Library

[6]

S. Bansal and A. Aiken. Binary translation using peephole superoptimizers. In OSDI, 2008.

Digital Library

[7]

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. An efficient method of computing static single assignment form. In POPL, 1989.

Digital Library

[8]

B. Fischer and J. Schumann. Autobayes: A system for generating data analysis programs from statistical models. J. Funct. Program., 13(3):483--508, 2003.

Digital Library

[9]

P. Flener and L. Popelmnsky. On the use of inductive reasoning in program synthesis: Prejudice and prospects. In LOBSTR. 1994.

Digital Library

[10]

E. M. Gold. Language identification in the limit. Information and Control, 10(5):447--474, 1967.

[11]

T. Granlund and R. Kenner. Eliminating branches using a superoptimizer and %the gnu c compiler. In PLDI, 1992.

Digital Library

[12]

S. Gulwani. Dimensions in program synthesis. In PPDP, pages 13--24. ACM, 2010.

Digital Library

[13]

S. Gulwani. Automating string processing in spreadsheets using input-output examples. In POPL, 2011.

Digital Library

[14]

S. Gulwani, V. Korthikanti, and A. Tiwari. Synthesizing geometry constructions. In PLDI, 2011.

Digital Library

[15]

J. Hamza, B. Jobstmann, and V. Kuncak. Synthesis for regular specifications over unbounded domains. In FMCAD, 2010.

Digital Library

[16]

B. Harris and S. Gulwani. Spreadsheet table transformations from examples. In PLDI, 2011.

Digital Library

[17]

S. Itzhaky, S. Gulwani, N. Immerman, and M. Sagiv. A simple inductive synthesis methodology and its applications. In OOPSLA, pages 36--46, 2010.

Digital Library

[18]

R. N. Jackiw and W. F. Finzer. The geometer's sketchpad: programming by geometry. In Watch what I do: programming by demonstration, pages 293--307. MIT Press, 1993.

Digital Library

[19]

S. Jha, S. Gulwani, S. Seshia, and A. Tiwari. Oracle-guided component-based program synthesis. In ICSE, pages 215--224, 2010.

Digital Library

[20]

S. Jha, S. Gulwani, S. Seshia, and A. Tiwari. Synthesizing switching logic for safety and dwell-time requirements. In Proc. 1st ACM/IEEE Intl. Conf. on Cyber-Physical Systems, ICCPS, pages 22--31, 2010.

Digital Library

[21]

T. A. Johnson and R. Eigenmann. Context-sensitive domain-independent algorithm composition and selection. In PLDI, 2006.

Digital Library

[22]

R. Joshi, G. Nelson, and K. H. Randall. Denali: A goal-directed superoptimizer. In PLDI, 2002.

Digital Library

[23]

D. E. Knuth. The art of computer programming. \URLhttp://www-cs-faculty.stanford.edu/ knuth/taocp.html.

[24]

T. A. Lau, P. Domingos, and D. S. Weld. Version space algebra and its application to programming by demonstration. In ICML, 2000.

Digital Library

[25]

Y. Lustig and M. Vardi. Synthesis from component libraries. In Proc. FoSSaCS, pages 395--409, 2009.

Digital Library

[26]

D. Mandelin, L. Xu, R. Bodík, and D. Kimelman. Jungloid mining: helping to navigate the API jungle. In PLDI, pages 48--61, 2005.

Digital Library

[27]

Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM TOPLAS, 2(1):90--121, 1980.

Digital Library

[28]

H. Massalin. Superoptimizer - a look at the smallest program. In ASPLOS, pages 122--126, 1987.

Digital Library

[29]

S. Muggleton, editor. Inductive Logic Programming, volume 38 of The APIC Series. Academic Press, 1992.

[30]

E. Y. Shapiro. Algorithmic Program DeBugging. MIT Press, Cambridge, MA, USA, 1983.

Digital Library

[31]

A. Solar-Lezama, G. Arnold, L. Tancau, R. Bodík, V. A. Saraswat, and S. A. Seshia. Sketching stencils. In PLDI, pages 167--178, 2007.

Digital Library

[32]

A. Solar-Lezama, R. Rabbah, R. Bodík, and K. Ebcioglu. Programming by sketching for bit-streaming programs. In PLDI, 2005.

Digital Library

[33]

A. Solar-Lezama, L. Tancau, R. Bodík, S. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006.

Digital Library

[34]

S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In POPL, pages 313--326, 2010.

Digital Library

[35]

M. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood. Deductive composition of astro. software from subroutine libraries. In CADE, '94.

Digital Library

[36]

A. Taly, S. Gulwani, and A. Tiwari. Synthesizing switching logic using constraint solving. In VMCAI, pages 305--319. Springer, 2009.

Digital Library

[37]

H. S. Warren. Hacker's Delight. Addison-Wesley, '02.

Digital Library

[38]

I. H. Witten and D. Mo. TELS: learning text editing tasks from examples. In Watch what I do: programming by demonstration, pages 293--307. MIT Press, Cambridge, MA, USA, 1993.

Digital Library

Cited By

Ding YQiu X(2024)Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector ManipulationsProceedings of the ACM on Programming Languages10.1145/36329138:POPL(2129-2159)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632913
Mell SZdancewic SBastani O(2024)Optimal Program Synthesis via Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36328588:POPL(457-481)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632858
Iannopollo AIncer ISangiovanni-Vincentelli A(2024)Synthesizing LTL contracts from component libraries using rich counterexamplesScience of Computer Programming10.1016/j.scico.2024.103116236:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103116
Show More Cited By

Recommendations

Synthesis of loop-free programs
PLDI '11

We consider the problem of synthesizing loop-free programs that implement a desired functionality using components from a given library. Specifications of the desired functionality and the library components are provided as logical relations between ...
FrAngel: component-based synthesis with control structures

In component-based program synthesis, the synthesizer generates a program given a library of components (functions). Existing component-based synthesizers have difficulty synthesizing loops and other control structures, and they often require formal ...
Can reactive synthesis and syntax-guided synthesis be friends?
SPLASH Companion 2021: Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2011

668 pages

ISBN:9781450306638

DOI:10.1145/1993498

General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

ACM SIGPLAN Notices Volume 46, Issue 6
PLDI '11
June 2011
652 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1993316
Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '11

Sponsor:

SIGPLAN

PLDI '11: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 4 - 8, 2011

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

257
Total Citations
View Citations
1,735
Total Downloads

Downloads (Last 12 months)95
Downloads (Last 6 weeks)6

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ding YQiu X(2024)Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector ManipulationsProceedings of the ACM on Programming Languages10.1145/36329138:POPL(2129-2159)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632913
Mell SZdancewic SBastani O(2024)Optimal Program Synthesis via Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36328588:POPL(457-481)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632858
Iannopollo AIncer ISangiovanni-Vincentelli A(2024)Synthesizing LTL contracts from component libraries using rich counterexamplesScience of Computer Programming10.1016/j.scico.2024.103116236:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103116
Hu JChong SSeltzer M(2024)Parallel Assembly SynthesisLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_1(3-26)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71294-4_1
Johnson KReynolds AReps TD’Antoni L(2024)The SemGuS ToolkitComputer Aided Verification10.1007/978-3-031-65633-0_2(27-40)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_2
Kim JSo SOh HGrundy JPollock LPenta M(2023)DIVER: Oracle-Guided SMT Solver Testing with Unrestricted Random MutationsProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00187(2224-2236)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00187
Kalita PSingal DAgarwal PJhunjhunwala SRoy S(2023)Symbolic encoding of LL(1) parsing and its applicationsFormal Methods in System Design10.1007/s10703-023-00420-361:2-3(338-379)Online publication date: 22-Jun-2023
https://doi.org/10.1007/s10703-023-00420-3
Agarwal AArun VRay DMartins RSeshan S(2022)Automating network heuristic design and analysisProceedings of the 21st ACM Workshop on Hot Topics in Networks10.1145/3563766.3564085(8-16)Online publication date: 14-Nov-2022
https://dl.acm.org/doi/10.1145/3563766.3564085
Muduli SRoy S(2022)Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzingProceedings of the ACM on Programming Languages10.1145/35633326:OOPSLA2(1236-1263)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563332
Wang CYao PTang WShi QZhang C(2022)Complexity-guided container replacement synthesisProceedings of the ACM on Programming Languages10.1145/35273126:OOPSLA1(1-31)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527312
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents