Skip to main content
SpringerLink
Log in

From Concrete Examples to Heap Manipulating Programs

  • Conference paper
Static Analysis (SAS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7935))

Included in the following conference series:

Abstract

Data-structure manipulation is not just a perplexing ordeal for newbies, but also a tedious errand for seasoned programmers. Even after a programmer gets the "hang of things", programming complex pointer manipulations (like reversing a linked list) still makes one reach for a notebook to draw some box-and-arrow diagrams to work out the low-level pointer jugglery. These diagrams are, not surprisingly, used as a basic tool to introduce heap manipulations in introductory programming courses.

We propose a synthesis technology to automatically create programs that manipulate heap data-structures from such diagrams. The programmer is needed to provide a set of concrete examples of her high-level strategy for the low-level manipulations to be discharged automatically. We plan the synthesis task as a sequence of "fast" stages, making it usable in an integrated development environment. We envisage that such a tool will be useful to programmers as a code-assist comfortably tucked away in their favorite integrated development environment.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: ESEC/FSE 2011, pp. 289–299. ACM, New York (2011)

    Google Scholar 

  2. Singh, R., Solar-Lezama, A.: SPT: Storyboard programming tool. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 738–743. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Solar Lezama, A.: Program Synthesis By Sketching. PhD thesis, EECS Department, University of California, Berkeley (December 2008)

    Google Scholar 

  4. Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4–13. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL 2011, pp. 317–330. ACM, New York (2011)

    Google Scholar 

  7. Gulwani, S., Harris, W.R., Singh, R.: Spreadsheet data manipulation using examples. Communications of the ACM (2012)

    Google Scholar 

  8. Harris, W.R., Gulwani, S.: Spreadsheet table transformations from examples. In: PLDI 2011, pp. 317–328. ACM, New York (2011)

    Google Scholar 

  9. Singh, R., Gulwani, S.: Learning semantic string transformations from examples. Proc. VLDB Endow. 5(8), 740–751 (2012)

    Google Scholar 

  10. Biermann, A.W., Baum, R.I., Petry, F.E.: Speeding up the synthesis of programs from traces. IEEE Trans. Comput. 24(2), 122–136 (1975)

    Article  MATH  Google Scholar 

  11. Cypher, A., Halbert, D.C., Kurlander, D., Lieberman, H., Maulsby, D., Myers, B.A., Turransky, A.: Watch what I do: programming by demonstration. MIT Press, Cambridge (1993)

    Google Scholar 

  12. Lau, T., Domingos, P., Weld, D.S.: Learning programs from traces using version space algebra. In: K-CAP 2003, pp. 36–43. ACM, New York (2003)

    Google Scholar 

  13. Solar-Lezama, A., Rabbah, R., Bodík, R., Ebcioğlu, K.: Programming by sketching for bit-streaming programs. In: PLDI 2005, pp. 281–294. ACM, New York (2005)

    Google Scholar 

  14. Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS-XII, pp. 404–415. ACM, New York (2006)

    Chapter  Google Scholar 

  15. Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI 2011, pp. 62–73. ACM, New York (2011)

    Google Scholar 

  16. Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE 2010, pp. 215–224. ACM, New York (2010)

    Google Scholar 

  17. Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL 2010, pp. 313–326. ACM, New York (2010)

    Google Scholar 

  18. Armando, A., Smaill, A., Green, I.: Automatic synthesis of recursive programs: The proof-planning paradigm. Automated Software Engg. 6(4), 329–356 (1999)

    Article  Google Scholar 

  19. Banerjee, D.: A methodology for synthesis of recursive functional programs. ACM Trans. Program. Lang. Syst. 9(3), 441–462 (1987)

    Article  MATH  Google Scholar 

  20. Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC/FSE-13, pp. 263–272. ACM, New York (2005)

    Chapter  Google Scholar 

  21. Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: ASPLOS-XII, pp. 394–403. ACM, New York (2006)

    Chapter  Google Scholar 

  22. Bansal, S., Aiken, A.: Binary translation using peephole superoptimizers. In: OSDI 2008, pp. 177–192. USENIX Association, Berkeley (2008)

    Google Scholar 

  23. Massalin, H.: Superoptimizer: a look at the smallest program. In: ASPLOS-II, pp. 122–126. IEEE Computer Society Press, Los Alamitos (1987)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science and Engineering Department, Indian Institute of Technology Kanpur, India

    Subhajit Roy

Authors
  1. Subhajit Roy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052, Redmond, WA, USA

    Francesco Logozzo

  2. One Microsoft Way, Microsoft Research, 98052, Redmond,, WA,, USA

    Manuel Fähndrich

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Roy, S. (2013). From Concrete Examples to Heap Manipulating Programs. In: Logozzo, F., Fähndrich, M. (eds) Static Analysis. SAS 2013. Lecture Notes in Computer Science, vol 7935. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38856-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38856-9_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38855-2

  • Online ISBN: 978-3-642-38856-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation