research-article

A simple inductive synthesis methodology and its applications

Authors:

Shachar Itzhaky,

Sumit Gulwani,

Neil Immerman,

Mooly SagivAuthors Info & Claims

OOPSLA '10: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

Pages 36 - 46

https://doi.org/10.1145/1869459.1869463

Published: 17 October 2010 Publication History

Get Access

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].

References

[1]

}}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.

Digital Library

Google Scholar

[2]

}}Yanhong A. Liu and Tim Teitelbaum. Systematic derivation of incremental programs. Sci. Comput. Program., 24(1):1--39, 1995.

Digital Library

Google Scholar

[3]

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

Google Scholar

[4]

}}Robert Paige.Formal Differentiation - A Program Synthesis Technique. UMI Press, 1981.

Google Scholar

[5]

}}Saurabh Srivastava, Sumit Gulwani, and Jeff Foster. From program verification to program synthesis. In POPL, pages 313--326, 2010.

Digital Library

Google Scholar

[6]

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

Digital Library

Google Scholar

[7]

}}Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006.

Digital Library

Google Scholar

[8]

}}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

[9]

}}Jiazhen Cai and Robert Paige. Binding performance at language design time. In POPL, pages 85--97, 1987.

Digital Library

Google Scholar

[10]

}}Leonardo de Moura and Nikolaj Bjørner. Z3 an efficient smt solver.http://research. microsoft.com/en-us/um/redmond/ projects/z3/.

Google Scholar

[11]

}}Pierre Flener and Lubos Popelmnsky. On the use of inductive reasoning in program synthesis: Prejudice and prospects. In LOBSTR'94. 1994.

Digital Library

Google Scholar

[12]

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

Crossref

Google Scholar

[13]

}}Neil Immerman. Descriptive Complexity. Springer, New York, 1999.

Google Scholar

Cited By

View all

Handa SRinard MDevanbu PCohen MZimmermann T(2020)Inductive program synthesis over noisy dataProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409732(87-98)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3368089.3409732
Bansal KKoskinen ETripp O(2020)Synthesizing Precise and Useful Commutativity ConditionsJournal of Automated Reasoning10.1007/s10817-020-09573-wOnline publication date: 29-Aug-2020
https://doi.org/10.1007/s10817-020-09573-w
Qin YWang HXu CMa XLu J(2018)SynEva: Evaluating ML Programs by Mirror Program Synthesis2018 IEEE International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS.2018.00031(171-182)Online publication date: Jul-2018
https://doi.org/10.1109/QRS.2018.00031
Show More Cited By

Index Terms

A simple inductive synthesis methodology and its applications
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

A simple inductive synthesis methodology and its applications
OOPSLA '10

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 ...
Dimensions in program synthesis
PPDP '10: Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming

Program 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 ...
Path-based inductive synthesis for program inversion
PLDI '11

In this paper, we investigate the problem of semi-automated inversion of imperative programs, which has the potential to make it much easier and less error prone to write programs that naturally pair as inverses, such as insert/delete operations, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

OOPSLA '10: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

October 2010

984 pages

ISBN:9781450302036

DOI:10.1145/1869459

General Chairs:
William R. Cook
University of Texas at Austin
,
Siobhán Clarke
Trinity College Dublin
,
Program Chairs:
Martin Rinard
MIT
,
Kevin J. Sullivan
University of Virginia
,
Daniel H. Steinberg
Dim Sum Thinking Inc.

ACM SIGPLAN Notices Volume 45, Issue 10
OOPSLA '10
October 2010
957 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1932682
Issue’s Table of Contents

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 October 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '10

Sponsor:

SIGPLAN

SPLASH '10: Systems Programming Languages and Applications: Software for Humanity

October 17 - 21, 2010

Nevada, Reno/Tahoe, USA

Acceptance Rates

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

41
Total Citations
View Citations
610
Total Downloads

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

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Handa SRinard MDevanbu PCohen MZimmermann T(2020)Inductive program synthesis over noisy dataProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409732(87-98)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3368089.3409732
Bansal KKoskinen ETripp O(2020)Synthesizing Precise and Useful Commutativity ConditionsJournal of Automated Reasoning10.1007/s10817-020-09573-wOnline publication date: 29-Aug-2020
https://doi.org/10.1007/s10817-020-09573-w
Qin YWang HXu CMa XLu J(2018)SynEva: Evaluating ML Programs by Mirror Program Synthesis2018 IEEE International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS.2018.00031(171-182)Online publication date: Jul-2018
https://doi.org/10.1109/QRS.2018.00031
Jangda AYorsh GTorlak EStorm TBiddle R(2017)Unbounded superoptimizationProceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3133850.3133856(78-88)Online publication date: 25-Oct-2017
https://dl.acm.org/doi/10.1145/3133850.3133856
Abate ABessa ICattaruzza DCordeiro LDavid CKesseli PKroening DFrehse GMitra S(2017)Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous PlantsProceedings of the 20th International Conference on Hybrid Systems: Computation and Control10.1145/3049797.3049802(197-206)Online publication date: 13-Apr-2017
https://dl.acm.org/doi/10.1145/3049797.3049802
Abate ABessa ICattaruzza DCordeiro LDavid CKesseli PKroening DPolgreen E(2017)Automated Formal Synthesis of Digital Controllers for State-Space Physical PlantsComputer Aided Verification10.1007/978-3-319-63387-9_23(462-482)Online publication date: 13-Jul-2017
https://doi.org/10.1007/978-3-319-63387-9_23
Lundquist GMohan VHamlen KGates CBöhme REgelman SMannan M(2016)Searching for software diversityProceedings of the 2016 New Security Paradigms Workshop10.1145/3011883.3011891(80-91)Online publication date: 26-Sep-2016
https://dl.acm.org/doi/10.1145/3011883.3011891
Neider DTopcu U(2016)An Automaton Learning Approach to Solving Safety Games over Infinite GraphsProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_12(204-221)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_12
Prountzos DManevich RPingali K(2015)Synthesizing parallel graph programs via automated planningACM SIGPLAN Notices10.1145/2813885.273795350:6(533-544)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737953
Prountzos DManevich RPingali KGrove DBlackburn S(2015)Synthesizing parallel graph programs via automated planningProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2737953(533-544)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2737953
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.

Cited By

Index Terms

Recommendations

A simple inductive synthesis methodology and its applications

Dimensions in program synthesis

Path-based inductive synthesis for program inversion