Shachar Itzhaky
Sumit Gulwani
Neil Immerman
ABSTRACT
Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an efficient program that meets the specification. In this paper, we present a new algorithmic methodology for inductive synthesis that allows us to do this.
We use Second Order logic as our generic high level specification logic. For our low-level languages we choose small application-specific logics that can be immediately translated into code that runs in expected linear time in the worst case.
We explain our methodology and provide examples of the synthesis of several graph classifiers, e.g, linear-time tests of whether the input graph is connected, acyclic, etc. In another set of applications we automatically derive many finite differencing expressions equivalent to ones that Paige built by hand in his thesis [Pai81]. Finally we describe directions for automatically combining such automatically generated building blocks to synthesize efficient code implementing more complicated specifications.
The methods in this paper have been implemented in Python using the SMT solver Z3 [dMB].
- }}Yanhong A. Liu and Scott D. Stoller. From datalog rules to efficient programs with time and space guarantees. ACM Trans. Program. Lang. Syst., 31(6), 2009. Google Scholar
Digital Library
- }}Yanhong A. Liu and Tim Teitelbaum. Systematic derivation of incremental programs. Sci. Comput. Program., 24(1):1--39, 1995. Google ScholarDigital Library
- }}Stephen Muggleton, editor. Inductive Logic Programming, volume 38 of The APIC Series. Academic Press, 1992.Google Scholar
- }}Robert Paige.Formal Differentiation - A Program Synthesis Technique. UMI Press, 1981.Google Scholar
- }}Saurabh Srivastava, Sumit Gulwani, and Jeff Foster. From program verification to program synthesis. In POPL, pages 313--326, 2010. Google ScholarDigital Library
- }}Ehud Y. Shapiro. Algorithmic Program DeBugging. MIT Press, Cambridge, MA, USA, 1983. Google ScholarDigital Library
- }}Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006. Google ScholarDigital Library
- }}B.A. Brandin, R. Malik, and P. Malik.Incremental verification and synthesis of discrete-event systems guided by counter examples. Control Systems Technology, 12(3), May 2004.Google Scholar
- }}Jiazhen Cai and Robert Paige. Binding performance at language design time. In POPL, pages 85--97, 1987. Google ScholarDigital Library
- }}Leonardo de Moura and Nikolaj Bjørner. Z3 an efficient smt solver.http://research. microsoft.com/en-us/um/redmond/ projects/z3/.Google Scholar
- }}Pierre Flener and Lubos Popelmnsky. On the use of inductive reasoning in program synthesis: Prejudice and prospects. In LOBSTR'94. 1994. Google ScholarDigital Library
- }}E. Mark Gold. Language identification in the limit. Information and Control, 10(5):447--474, 1967.Google ScholarCross Ref
- }}Neil Immerman. Descriptive Complexity. Springer, New York, 1999.Google Scholar
Index Terms
- A simple inductive synthesis methodology and its applications
Recommendations
FlashMeta: a framework for inductive program synthesis
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and ApplicationsInductive synthesis, or programming-by-examples (PBE) is gaining prominence with disruptive applications for automating repetitive tasks in end-user programming. However, designing, developing, and maintaining an effective industrial-quality inductive ...
A simple inductive synthesis methodology and its applications
OOPSLA '10Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an efficient program that meets the specification. In this paper, we present a new algorithmic methodology for inductive synthesis that allows ...
Dimensions in program synthesis
PPDP '10: Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programmingProgram Synthesis, which is the task of discovering programs that realize user intent, can be useful in several scenarios: enabling people with no programming background to develop utility programs, helping regular programmers automatically discover ...
Comments