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

research-article

Open access

Relational program synthesis

Authors:

Isil DilligAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue OOPSLA

Article No.: 155, Pages 1 - 27

https://doi.org/10.1145/3276525

Published: 24 October 2018 Publication History

Abstract

This paper proposes relational program synthesis, a new problem that concerns synthesizing one or more programs that collectively satisfy a relational specification. As a dual of relational program verification, relational program synthesis is an important problem that has many practical applications, such as automated program inversion and automatic generation of comparators. However, this relational synthesis problem introduces new challenges over its non-relational counterpart due to the combinatorially larger search space. As a first step towards solving this problem, this paper presents a synthesis technique that combines the counterexample-guided inductive synthesis framework with a novel inductive synthesis algorithm that is based on relational version space learning. We have implemented the proposed technique in a framework called Relish, which can be instantiated to different application domains by providing a suitable domain-specific language and the relevant relational specification. We have used the Relish framework to build relational synthesizers to automatically generate string encoders/decoders as well as comparators, and we evaluate our tool on several benchmarks taken from prior work and online forums. Our experimental results show that the proposed technique can solve almost all of these benchmarks and that it significantly outperforms EUSolver, a generic synthesis framework that won the general track of the most recent SyGuS competition.

Supplementary Material

WEBM File (a155-wang.webm)

Download
90.96 MB

References

[1]

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In Proc. of FMCAD. 1–8.

[2]

Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In Proc. of TACAS. 319–336.

[3]

Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational verification using product programs. In Proc. of FM. Springer, 200–214.

Digital Library

[4]

Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2013. Beyond 2-safety: Asymmetric product programs for relational program verification. In Proc. of LFCS. Springer, 29–43.

[5]

Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2016. Product programs and relational program logics. Journal of Logical and Algebraic Methods in Programming 85, 5 (2016), 847–859.

[6]

Gilles Barthe, Pedro R D’Argenio, and Tamara Rezk. 2004. Secure information flow by self-composition. In Proc. of CSF. 100–114.

Digital Library

[7]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2012a. Probabilistic relational Hoare logics for computeraided security proofs. In International Conference on Mathematics of Program Construction. Springer, 1–6.

Digital Library

[8]

Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2012b. Probabilistic relational reasoning for differential privacy. In Proc. of POPL, Vol. 47. 97–110.

Digital Library

[9]

Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. In Proc. of POPL, Vol. 39. 14–25.

Digital Library

[10]

Jia Chen, Yu Feng, and Isil Dillig. 2017. Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic. In Proc. of CCS. 875–890.

Digital Library

[11]

Wei Chen and Jan Tijmen Udding. 1990. Program inversion: More than fun! Science of Comp. Prog. 15, 1 (1990), 1–13.

Digital Library

[12]

Hubert Comon. 1997. Tree automata techniques and applications. http://www. grappa. univ-lille3. fr/tata (1997).

[13]

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. 2016. Relational verification through horn clause transformation. In Proc. of SAS. Springer, 147–169.

[14]

Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proc. of POPL, Vol. 50. 689–700.

Digital Library

[15]

Edsger W Dijkstra. 1982. Program inversion. In Selected Writings on Computing: A Personal Perspective. Springer, 351–354.

Digital Library

[16]

John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing data structure transformations from input-output examples. In Proc. of PLDI. 229–239.

Digital Library

[17]

Giorgio Gallo, Giustino Longo, Stefano Pallottino, and Sang Nguyen. 1993. Directed hypergraphs and applications. Discrete applied mathematics 42, 2-3 (1993), 177–201.

Digital Library

[18]

Cordell Green. 1969. Application of theorem proving to problem solving. In Proc. of IJCAI. 219–239.

Digital Library

[19]

Sumit Gulwani. 2011. Automating string processing in spreadsheets using input-output examples. In Proc. of POPL. 317–330.

Digital Library

[20]

Sumit Gulwani. 2012. Synthesis from examples: Interaction models and algorithms. In Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) . 8–14.

Digital Library

[21]

Stefan Heule, Eric Schkufza, Rahul Sharma, and Alex Aiken. 2016. Stratified synthesis: automatically learning the x86-64 instruction set. In Proc. of PLDI. 237–250.

Digital Library

[22]

Qinheping Hu and Loris D’Antoni. 2017. Automatic program inversion using symbolic transducers. In Proc. of PLDI. 376–389.

Digital Library

[23]

Barbara Jobstmann, Andreas Griesmayer, and Roderick Bloem. 2005. Program repair as a game. In Proc. of CAV. 226–238.

Digital Library

[24]

Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013. Synthesis modulo recursive functions. Proc. of OOPSLA 48, 10 (2013), 407–426.

Digital Library

[25]

Tessa Lau, Steven A. Wolfman, Pedro Domingos, and Daniel S. Weld. 2003. Programming by Demonstration Using Version Space Algebra. Machine Learning 53, 1-2 (2003), 111–156.

Digital Library

[26]

Zohar Manna and Richard Waldinger. 1986. A deductive approach to program synthesis. In Readings in artificial intelligence and software engineering . Elsevier, 3–34.

Digital Library

[27]

Tom M Mitchell. 1982. Generalization as search. Artificial intelligence 18, 2 (1982), 203–226.

[28]

Dmitry Mordvinov and Grigory Fedyukovich. 2017. Synchronizing constrained Horn clauses. LPAR, EPiC Series in Computing (2017).

[29]

Carroll Morgan. 1994. Programming from specifications. Prentice Hall.

Digital Library

[30]

Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury, and Satish Chandra. 2013. Semfix: Program repair via semantic analysis. In Proc. of ICSE. 772–781.

Digital Library

[31]

Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In Proc. of PLDI. 522–538.

Digital Library

[32]

Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: A framework for inductive program synthesis. In Proc. of OOPSLA, Vol. 50. 107–126.

Digital Library

[33]

Veselin Raychev, Pavol Bielik, Martin T. Vechev, and Andreas Krause. 2016. Learning programs from noisy data. In Proc. of POPL . 761–774.

Digital Library

[34]

Veselin Raychev, Martin T. Vechev, and Andreas Krause. 2015. Predicting Program Properties from "Big Code". In Proc. of POPL . 111–124.

Digital Library

[35]

Brian J Ross. 1997. Running programs backwards: the logical inversion of imperative computation. Formal Aspects of Computing 9, 3 (1997), 331–348.

[36]

Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic superoptimization. In Proc. of ASPLOS. 305–316.

Digital Library

[37]

Sunbeom So and Hakjoo Oh. 2017. Synthesizing Imperative Programs from Examples Guided by Static Analysis. In Proc. of SAS . 364–381.

[38]

Armando Solar-Lezama. 2008. Program synthesis by sketching. University of California, Berkeley.

[39]

Armando Solar-Lezama. 2009. The sketching approach to program synthesis. In Proc. of APLAS. Springer, 4–13.

Digital Library

[40]

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial sketching for finite programs. Proc. of ASPLOS 41, 11 (2006), 404–415.

Digital Library

[41]

Marcelo Sousa and Isil Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In Proc. of PLDI. 57–69.

Digital Library

[42]

Marcelo Sousa, Isil Dillig, and Shuvendu K. Lahiri. 2018. Verified Three-Way Program Merge. PACMPL OOPSLA (2018).

Digital Library

[43]

Marcelo Sousa, Isil Dillig, Dimitrios Vytiniotis, Thomas Dillig, and Christos Gkantsidis. 2014. Consolidation of queries with user-defined functions. In Proc. of PLDI, Vol. 49. 554–564.

Digital Library

[44]

Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, and Jeffrey S Foster. 2011. Path-based inductive synthesis for program inversion. In Proc. of PLDI, Vol. 46. 492–503.

Digital Library

[45]

Xinyu Wang, Isil Dillig, and Rishabh Singh. 2017. Synthesis of data completion scripts using finite tree automata. PACMPL 1, OOPSLA (2017), 62:1–62:26.

Digital Library

[46]

Xinyu Wang, Isil Dillig, and Rishabh Singh. 2018a. Program synthesis using abstraction refinement. PACMPL 2, POPL (2018), 63:1–63:30.

Digital Library

[47]

Xinyu Wang, Sumit Gulwani, and Rishabh Singh. 2016. FIDEX: filtering spreadsheet data using examples. In Proc. of OOPSLA. 195–213.

Digital Library

[48]

Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2018b. Verifying equivalence of database-driven applications. PACMPL 2, POPL (2018), 56:1–56:29.

Digital Library

[49]

Yuepeng Wang, Xinyu Wang, and Isil Dillig. 2018c. Relational Program Synthesis. http://arxiv.org/abs/1809.02283 . arXiv: 1809.02283

[50]

Navid Yaghmazadeh, Xinyu Wang, and Isil Dillig. 2018. Automated Migration of Hierarchical Data to Relational Tables using Programming-by-Example. Proc. of VLDB 11, 5 (2018), 580–593.

Digital Library

[51]

Hongseok Yang. 2007. Relational separation logic. Theoretical Computer Science 375, 1-3 (2007), 308–334.

Digital Library

[52]

Anna Zaks and Amir Pnueli. 2008. Covac: Compiler validation by program analysis of the cross-product. In Proc. of FM. Springer, 35–51.

Digital Library

Cited By

Nguyen Trong BTsushima KHu Z(2024)S_YNTHBX: An Example-guided Synthesizer for Bidirectional Programs on RelationsJournal of Information Processing10.2197/ipsjjip.32.47132(471-486)Online publication date: 2024
https://doi.org/10.2197/ipsjjip.32.471
Wang ZPailoor SPrakash AWang YDillig I(2024)From Batch to Stream: Automatic Generation of Online AlgorithmsProceedings of the ACM on Programming Languages10.1145/36564188:PLDI(1014-1039)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656418
Li XZhou XDong RZhang YWang X(2024)Efficient Bottom-Up Synthesis for Programs with Local VariablesProceedings of the ACM on Programming Languages10.1145/36328948:POPL(1540-1568)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632894
Show More Cited By

Index Terms

Relational program synthesis
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Automatic programming
  2. Software notations and tools
    1. Context specific languages
      1. Programming by example
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

Algorithmic program synthesis: introduction

Program synthesis is a process of producing an executable program from a specification. Algorithmic synthesis produces the program automatically, without an intervention from an expert. While classical compilation falls under the definition of ...
From program verification to program synthesis
POPL '10

This paper describes a novel technique for the synthesis of imperative programs. Automated program synthesis has the potential to make programming and the design of systems easier by allowing programs to be specified at a higher-level than executable ...
Synthesising Programs with Non-trivial Constants
Abstract
Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. While ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue OOPSLA

November 2018

1656 pages

EISSN:2475-1421

DOI:10.1145/3288538

Issue’s Table of Contents

Copyright © 2018 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2018

Published in PACMPL Volume 2, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
911
Total Downloads

Downloads (Last 12 months)151
Downloads (Last 6 weeks)19

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Nguyen Trong BTsushima KHu Z(2024)S_YNTHBX: An Example-guided Synthesizer for Bidirectional Programs on RelationsJournal of Information Processing10.2197/ipsjjip.32.47132(471-486)Online publication date: 2024
https://doi.org/10.2197/ipsjjip.32.471
Wang ZPailoor SPrakash AWang YDillig I(2024)From Batch to Stream: Automatic Generation of Online AlgorithmsProceedings of the ACM on Programming Languages10.1145/36564188:PLDI(1014-1039)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656418
Li XZhou XDong RZhang YWang X(2024)Efficient Bottom-Up Synthesis for Programs with Local VariablesProceedings of the ACM on Programming Languages10.1145/36328948:POPL(1540-1568)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632894
Pailoor SWang YDillig I(2024)Semantic Code Refactoring for Abstract Data TypesProceedings of the ACM on Programming Languages10.1145/36328708:POPL(816-847)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632870
Miltner AWang ZChaudhuri SDillig I(2024)Relational Synthesis of Recursive Programs via Constraint Annotated Tree AutomataComputer Aided Verification10.1007/978-3-031-65633-0_3(41-63)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_3
Sun YPeng XXiong Y(2023)Synthesizing Efficient Memoization AlgorithmsProceedings of the ACM on Programming Languages10.1145/36228007:OOPSLA2(89-115)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622800
Yuan YRadhakrishna ASamanta R(2023)Trace-Guided Inductive Synthesis of Recursive Functional ProgramsProceedings of the ACM on Programming Languages10.1145/35912557:PLDI(860-883)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591255
Krogmeier PMadhusudan P(2023)Languages with Decidable Learning: A Meta-theoremProceedings of the ACM on Programming Languages10.1145/35860327:OOPSLA1(143-171)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586032
Miltner ANuñez ABrendel AChaudhuri SDillig I(2022)Bottom-up synthesis of recursive functional programs using angelic executionProceedings of the ACM on Programming Languages10.1145/34986826:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498682
Krogmeier PMadhusudan P(2022)Learning formulas in finite variable logicsProceedings of the ACM on Programming Languages10.1145/34986716:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498671
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Figures

Tables

Media

View Issue’s Table of Contents