More Web Proxy on the site http://driver.im/

research-article

Synthesizing data structure manipulations from storyboards

Authors:

Armando Solar-LezamaAuthors Info & Claims

ESEC/FSE '11: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering

Pages 289 - 299

https://doi.org/10.1145/2025113.2025153

Published: 09 September 2011 Publication History

Abstract

We present the Storyboard Programming framework, a new synthesis system designed to help programmers write imperative low-level data-structure manipulations. The goal of this system is to bridge the gap between the "boxes-and-arrows" diagrams that programmers often use to think about data-structure manipulation algorithms and the low-level imperative code that implements them. The system takes as input a set of partial input-output examples, as well as a description of the high-level structure of the desired solution. From this information, it is able to synthesize low-level imperative implementations in a matter of minutes.

The framework is based on a new approach for combining constraint-based synthesis and abstract-interpretation-based shape analysis. The approach works by encoding both the synthesis and the abstract interpretation problem as a constraint satisfaction problem whose solution defines the desired low-level implementation. We have used the framework to synthesize several data-structure manipulations involving linked lists and binary search trees, as well as an insertion operation into an And Inverter Graph.

References

[1]

http://cs.wellesley.edu/~cs231/fall01/red-black.pdf.

[2]

http://people.csail.mit.edu/rishabh/storyboard/.

[3]

Robert K. Brayton and Alan Mishchenko. ABC: An Academic Industrial-Strength Verification Tool. In CAV, pages 24--40, 2010.

Digital Library

[4]

James Brotherston, Richard Bornat, and Cristiano Calcagno. Cyclic proofs of program termination in separation logic. In POPL, pages 101--112, 2008.

Digital Library

[5]

Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252, 1977.

Digital Library

[6]

Allen Cypher, Daniel C. Halbert, David Kurlander, Henry Lieberman, David Maulsby, Brad A. Myers, and Alan Turransky, editors. Watch what I do: programming by demonstration. MIT Press, Cambridge, MA, USA, 1993.

Digital Library

[7]

Pascal Fradet and Daniel Le Metayer. Shape types. In POPL, pages 27--39. ACM Press, 1997.

Digital Library

[8]

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

Digital Library

[9]

Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. Synthesis of loop-free programs. In PLDI, pages 62--73, 2011.

Digital Library

[10]

Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. Program analysis as constraint solving. In PLDI, pages 281--292, 2008.

Digital Library

[11]

Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. Constraint-based invariant inference over predicate abstraction. In VMCAI, 2009.

Digital Library

[12]

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, and Mooly Sagiv. Data representation synthesis. In PLDI, pages 38--49. ACM, 2011.

Digital Library

[13]

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

Digital Library

[14]

Barbara Jobstmann, Andreas Griesmayer, and Roderick Bloem. Program repair as a game. In CAV, pages 226--238, 2005.

Digital Library

[15]

Tal Lev-Ami and Shmuel Sagiv. Tvla: A system for implementing static analyses. In SAS, 2000.

Digital Library

[16]

Z. Manna and R. Waldinger. Synthesis: Dreams => programs. IEEE Transactions on Software Engineering, 5(4):294--328, 1979.

Digital Library

[17]

Zohar Manna and Richard Waldinger. A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst., 2(1):90--121, 1980.

Digital Library

[18]

A. Mishchenko, S. Chatterjee, R. Jiang, and R. K. Brayton. FRAIGs: A unifying representation for logic synthesis and verification. Technical report, EECS, UC Berkeley, 2005.

[19]

Huu Hai Nguyen, Cristina David, Shengchao Qin, and Wei ngan Chin. Automated verification of shape and size properties via separation logic. In In VMCAI. Springer, 2007.

Digital Library

[20]

Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In ICALP, pages 652--671, London, UK, 1989. Springer-Verlag.

Digital Library

[21]

Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. In POPL, pages 105--118. ACM, 1999.

Digital Library

[22]

Horst Samulowitz and Fahiem Bacchus. Binary clause reasoning in qbf. In SAT, pages 353--367, 2006.

Digital Library

[23]

M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S. Muchnick, N. Jones (Eds.), Program Flow Analysis: Theory and Applications, pages 189--234, 1981.

[24]

Armando Solar-Lezama. Program Synthesis By Sketching. PhD thesis, EECS, UC Berkeley, 2008.

Digital Library

[25]

Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, and Sanjit Seshia. Sketching stencils. In PLDI, pages 167--178, 2007.

Digital Library

[26]

Armando Solar-Lezama, Chris Jones, Gilad Arnold, and Rastislav Bodík. Sketching concurrent datastructures. In PLDI, 2008.

Digital Library

[27]

Armando Solar-Lezama, Rodric Rabbah, Rastislav Bodik, and Kemal Ebcioglu. Programming by sketching for bit-streaming programs. In PLDI, 2005.

Digital Library

[28]

Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, and Jeffrey S. Foster. Path-based inductive synthesis for program inversion. In PLDI, pages 492--503. ACM, 2011.

Digital Library

[29]

Saurabh Srivastava, Sumit Gulwani, and Jeffrey Foster. From program verification to program synthesis. POPL, 2010.

Digital Library

[30]

Martin Vechev and Eran Yahav. Deriving linearizable fine-grained concurrent objects. SIGPLAN Not., 43(6):125--135, 2008.

Digital Library

[31]

Martin Vechev, Eran Yahav, and Greta Yorsh. Abstraction-guided synthesis of synchronization. In POPL, New York, NY, USA, 2010. ACM.

Digital Library

Cited By

Yoon YLee WYi K(2023)Inductive Program Synthesis via Iterative Forward-Backward Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/35912887:PLDI(1657-1681)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591288
Hu JLu EHolland DKawaguchi MChong SSeltzer M(2023)Towards Porting Operating Systems with Program SynthesisACM Transactions on Programming Languages and Systems10.1145/356394345:1(1-70)Online publication date: 3-Mar-2023
https://dl.acm.org/doi/10.1145/3563943
Emerson ASullivan A(2023)Crucible: Graphical Test Cases for Alloy Models2023 IEEE 34th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE59848.2023.00065(218-227)Online publication date: 9-Oct-2023
https://doi.org/10.1109/ISSRE59848.2023.00065
Show More Cited By

Recommendations

Natural synthesis of provably-correct data-structure manipulations

This paper presents natural synthesis, which generalizes the proof-theoretic synthesis technique to support very expressive logic theories. This approach leverages the natural proof methodology and reduces an intractable, unbounded-size synthesis ...
Synthesizing transformations on hierarchically structured data
PLDI '16

This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-...
Synthesizing data structure transformations from input-output examples
PLDI '15

We present a method for example-guided synthesis of functional programs over recursive data structures. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ESEC/FSE '11: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering

September 2011

548 pages

ISBN:9781450304436

DOI:10.1145/2025113

General Chair:
Tibor Gyimóthy
University of Szeged, Hungary
,
Program Chair:
Andreas Zeller
Saarland University, Germany

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

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ESEC/FSE'11

Sponsor:

SIGSOFT

ESEC/FSE'11: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering

September 5 - 9, 2011

Szeged, Hungary

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

62
Total Citations
View Citations
469
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yoon YLee WYi K(2023)Inductive Program Synthesis via Iterative Forward-Backward Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/35912887:PLDI(1657-1681)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591288
Hu JLu EHolland DKawaguchi MChong SSeltzer M(2023)Towards Porting Operating Systems with Program SynthesisACM Transactions on Programming Languages and Systems10.1145/356394345:1(1-70)Online publication date: 3-Mar-2023
https://dl.acm.org/doi/10.1145/3563943
Emerson ASullivan A(2023)Crucible: Graphical Test Cases for Alloy Models2023 IEEE 34th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE59848.2023.00065(218-227)Online publication date: 9-Oct-2023
https://doi.org/10.1109/ISSRE59848.2023.00065
Chou SAmarasinghe S(2022)Compilation of dynamic sparse tensor algebraProceedings of the ACM on Programming Languages10.1145/35633386:OOPSLA2(1408-1437)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563338
Zang ZWiatrek NGligoric MShi A(2022)Compiler Testing using Template Java ProgramsProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3556958(1-13)Online publication date: 10-Oct-2022
https://dl.acm.org/doi/10.1145/3551349.3556958
Shi KBieber DSingh R(2022)TF-Coder: Program Synthesis for Tensor ManipulationsACM Transactions on Programming Languages and Systems10.1145/351703444:2(1-36)Online publication date: 27-May-2022
https://dl.acm.org/doi/10.1145/3517034
Nguyen TYadavally ANguyen T(2022)Phrase2Set: Phrase-to-Set Machine Translation and Its Software Engineering Applications2022 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER53432.2022.00068(502-513)Online publication date: Mar-2022
https://doi.org/10.1109/SANER53432.2022.00068
Verma SRoy S(2022)Debug-localize-repair: a symbiotic construction for heap manipulationsFormal Methods in System Design10.1007/s10703-021-00387-z58:3(399-439)Online publication date: 8-Feb-2022
https://doi.org/10.1007/s10703-021-00387-z
Gao XRadhakrishna ASoares GShariffdeen RGulwani SRoychoudhury A(2021)APIfix: output-oriented program synthesis for combating breaking changes in librariesProceedings of the ACM on Programming Languages10.1145/34855385:OOPSLA(1-27)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485538
Bavishi RLemieux CSen KStoica I(2021)Gauss: program synthesis by reasoning over graphsProceedings of the ACM on Programming Languages10.1145/34855115:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485511
Show More Cited By

View Options

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.

Figures

Tables

Media

View Table of Conten