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

research-article

Synthesis modulo recursive functions

Authors:

Etienne Kneuss,

Philippe SuterAuthors Info & Claims

OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

Pages 407 - 426

https://doi.org/10.1145/2509136.2509555

Published: 29 October 2013 Publication History

Abstract

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synthesis procedures for algebraic data types. We present new counterexample-guided algorithms for constructing verified programs. We have implemented these algorithms in an integrated environment for interactive verification and synthesis from relational specifications. Our system was able to synthesize a number of useful recursive functions that manipulate unbounded numbers and data structures.

References

[1]

A. Albarghouthi, S. Gulwani, and Z. Kincaid. Recursive program synthesis. In CAV, pages 934--950, 2013.

Digital Library

[2]

E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems, pages 1--20, 1994.

Digital Library

[3]

R.-J. Back and J. von Wright. Refinement Calculus. Springer-Verlag, 1998.

[4]

R. W. Blanc, E. Kneuss, V. Kuncak, and P. Suter. An overview of the Leon verification system: Verification by translation to recursive functions. In Scala Workshop, 2013.

Digital Library

[5]

C. Boyapati, S. Khurshid, and D. Marinov. Korat: automated testing based on java predicates. In ISSTA, pages 123--133, 2002. 10.1145/566172.566191.

Digital Library

[6]

M. Butler, J. Grundy, T. Langbacka, R. Ruksenas, and J. von Wright. The refinement calculator: Proof support for program refinement. In Formal Methods Pacific, 1997.

[7]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337--340, 2008.

Digital Library

[8]

L. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, 2009.

[9]

P. Flener and D. Partridge. Inductive programming. Autom. Softw. Eng., 8 (2): 131--137, 2001.

Digital Library

[10]

M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak, and D. Marinov. Test generation through programming in UDITA. In ICSE, pages 225--234, 2010.

Digital Library

[11]

S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In PLDI, pages 62--73, 2011.

Digital Library

[12]

T. Gvero, V. Kuncak, I. Kuraj, and R. Piskac. Complete completion using types and weights. In PLDI, pages 27--38, 2013.

Digital Library

[13]

M. Hofmann. IgorII - an analytical inductive functional programming system (tool demo). In PEPM, pages 29--32, 2010.

Digital Library

[14]

D. Jackson. Structuring Z specifications with views. ACM Trans. Softw. Eng. Methodol., 4 (4): 365--389, 1995.

Digital Library

[15]

S. Jacobs, V. Kuncak, and P. Suter. Reductions for synthesis procedures. In VMCAI, pages 88--107, 2013.

Digital Library

[16]

J. Jaffar and J.-L. Lassez. Constraint logic programming. In POPL, pages 111--119, 1987.

Digital Library

[17]

B. Jobstmann and R. Bloem. Optimizations for LTL synthesis. In FMCAD, pages 117--124, 2006.

Digital Library

[18]

J. R. Josephson. Abductive Inference: Computation, Philosophy, Technology. Cambridge University Press, 1994.

[19]

A. C. Kakas, R. A. Kowalski, and F. Toni. Abductive logic programming. J. Log. Comput., 2 (6): 719--770, 1992.

[20]

E. Kitzelmann and U. Schmid. Inductive synthesis of functional programs: An explanation based generalization approach. JMLR, 7: 429--454, 2006.

Digital Library

[21]

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In SOSP, pages 207--220, 2009.

Digital Library

[22]

A. S. Köksal, V. Kuncak, and P. Suter. Constraints as control. In POPL, pages 151--164, 2012.

Digital Library

[23]

V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Complete functional synthesis. In PLDI, pages 316--329, 2010.

Digital Library

[24]

V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Software synthesis procedures. CACM, 55 (2): 103--111, 2012.

Digital Library

[25]

V. Kuncak, E. Kneuss, and P. Suter. Executing specifications using synthesis and constraint solving (invited talk). In Runtime Verification (RV), 2013.

[26]

I. Kuraj. Interactive code generation. Master's thesis, EPFL, 02 2013.

[27]

D. Leinenbach and T. Santen. Verifying the Microsoft Hyper-V hypervisor with VCC. In FM, pages 806--809, 2009.

Digital Library

[28]

Y. Lustig and M. Y. Vardi. Synthesis from component libraries. In FOSSACS, pages 395--409, 2009.

Digital Library

[29]

Z. Manna and R. J. Waldinger. Toward automatic program synthesis. Commun. ACM, 14 (3): 151--165, 1971.

Digital Library

[30]

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

Digital Library

[31]

A. Martelli and U. Montanari. Additive AND/OR graphs. In IJCAI, pages 1--11, 1973.

Digital Library

[32]

S. Muggleton and L. D. Raedt. Inductive logic programming: Theory and methods. J. Log. Program., 19/20: 629--679, 1994.

[33]

T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002.

Digital Library

[34]

C. Okasaki. Purely functional data structures. Cambridge University Press, 1999.

Digital Library

[35]

Y. Pei, Y. Wei, C. A. Furia, M. Nordio, and B. Meyer. Code-based automated program fixing. ArXiv e-prints, 2011. arXiv:1102.1059.

Digital Library

[36]

N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In VMCAI, pages 364--380, 2006.

Digital Library

[37]

A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, 1989.

Digital Library

[38]

R. Singh and S. Gulwani. Synthesizing number transformations from input-output examples. In CAV, pages 634--651, 2012.

Digital Library

[39]

D. R. Smith. Generating programs plus proofs by refinement. In VSTTE, pages 182--188, 2005.

[40]

A. Solar-Lezama, L. Tancau, R. Bodík, S. A. Seshia, and V. A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, pages 404--415, 2006.

Digital Library

[41]

A. Solar-Lezama, G. Arnold, L. Tancau, R. Bodík, V. A. Saraswat, and S. A. Seshia. Sketching stencils. In PLDI, pages 167--178, 2007.

Digital Library

[42]

A. Solar-Lezama, C. G. Jones, and R. Bodík. Sketching concurrent data structures. In PLDI, pages 136--148, 2008.

Digital Library

[43]

A. Spielmann, A. Nötzli, C. Koch, V. Kuncak, and Y. Klonatos. Automatic synthesis of out-of-core algorithms. In SIGMOD, 2013.

Digital Library

[44]

S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In POPL, pages 313--326, 2010.

Digital Library

[45]

P. D. Summers. A methodology for LISP program construction from examples. JACM, 24 (1): 161--175, 1977.

Digital Library

[46]

P. Suter. Programming with Specifications. PhD thesis, EPFL, December 2012.

[47]

P. Suter, M. Dotta, and V. Kuncak. Decision procedures for algebraic data types with abstractions. In POPL, pages 199--210, 2010.

Digital Library

[48]

P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive programs. In SAS, pages 298--315, 2011.

Digital Library

[49]

A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim, M. M. K. Martin, and R. Alur. TRANSIT: specifying protocols with concolic snippets. In PLDI, pages 287--296, 2013.

Digital Library

[50]

M. T. Vechev, E. Yahav, and G. Yorsh. Inferring synchronization under limited observability. In TACAS, pages 139--154, 2009.

Digital Library

[51]

C. von Essen and B. Jobstmann. Program repair without regret. In CAV, pages 896--911, 2013.

Digital Library

[52]

Y. Wei, C. A. Furia, N. Kazmin, and B. Meyer. Inferring better contracts. In ICSE, pages 191--200, 2011.

Digital Library

[53]

N. Wirth. Program development by stepwise refinement. Commun. ACM, 14 (4): 221--227, 1971.

Digital Library

Cited By

Hong QAiken A(2024)Recursive Program Synthesis using ParamorphismsProceedings of the ACM on Programming Languages10.1145/36563818:PLDI(102-125)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656381
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
Hozzová PAmrollahi DHajdu MKovács LVoronkov AWagner E(2024)Synthesis of Recursive Programs in SaturationAutomated Reasoning10.1007/978-3-031-63498-7_10(154-171)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_10
Show More Cited By

Index Terms

Synthesis modulo recursive functions

Recommendations

Synthesis modulo recursive functions
OOPSLA '13

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete ...
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for ...
Symbolic Automata: Omega-Regularity Modulo Theories

Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions and languages over finite words. In symbolic automata (or automata modulo A), an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

October 2013

904 pages

ISBN:9781450323741

DOI:10.1145/2509136

Co-chair:
Antony Hosking
Purdue University, USA
,
General Chair:
Patrick Eugster
Purdue University, USA
,
Program Chair:
Cristina V. Lopes
University of California, Irvine, USA

ACM SIGPLAN Notices Volume 48, Issue 10
OOPSLA '13
October 2013
867 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2544173
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2013 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 October 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '13

Sponsor:

SIGPLAN

SPLASH '13: Conference on Systems, Programming, and Applications: Software for Humanity

October 29 - 31, 2013

Indiana, Indianapolis, USA

Acceptance Rates

OOPSLA '13 Paper Acceptance Rate 50 of 189 submissions, 26%;

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

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

85
Total Citations
View Citations
575
Total Downloads

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

Reflects downloads up to 23 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Hong QAiken A(2024)Recursive Program Synthesis using ParamorphismsProceedings of the ACM on Programming Languages10.1145/36563818:PLDI(102-125)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656381
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
Hozzová PAmrollahi DHajdu MKovács LVoronkov AWagner E(2024)Synthesis of Recursive Programs in SaturationAutomated Reasoning10.1007/978-3-031-63498-7_10(154-171)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_10
Hughes JOrchard D(2024)Program Synthesis from Graded TypesProgramming Languages and Systems10.1007/978-3-031-57262-3_4(83-112)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_4
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
Fiala JItzhaky SMüller PPolikarpova NSergey I(2023)Leveraging Rust Types for Program SynthesisProceedings of the ACM on Programming Languages10.1145/35912787:PLDI(1414-1437)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591278
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
Lee WCho H(2023)Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive ExpressionsProceedings of the ACM on Programming Languages10.1145/35712637:POPL(2048-2078)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571263
Farzan ANicolet V(2023)Partial bounding for recursive function synthesisFormal Methods in System Design10.1007/s10703-023-00417-y63:1-3(172-205)Online publication date: 16-May-2023
https://doi.org/10.1007/s10703-023-00417-y
Costa Seco JAldrich JCarvalho LToninho BFerreira CScholliers CSinger J(2022)Derivations with Holes for Concept-Based Program SynthesisProceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3563835.3567658(63-79)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563835.3567658
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.

Media

Figures

Other

Tables

View Table of Contents