Etienne Kneuss
Viktor Kuncak
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.
- A. Albarghouthi, S. Gulwani, and Z. Kincaid. Recursive program synthesis. In CAV, pages 934--950, 2013. Google Scholar
Digital Library
- E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems, pages 1--20, 1994. Google ScholarDigital Library
- R.-J. Back and J. von Wright. Refinement Calculus. Springer-Verlag, 1998.Google Scholar
- 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. Google ScholarDigital Library
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: automated testing based on java predicates. In ISSTA, pages 123--133, 2002. 10.1145/566172.566191. Google ScholarDigital Library
- 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.Google Scholar
- L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337--340, 2008. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, 2009.Google ScholarCross Ref
- P. Flener and D. Partridge. Inductive programming. Autom. Softw. Eng., 8 (2): 131--137, 2001. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In PLDI, pages 62--73, 2011. Google ScholarDigital Library
- T. Gvero, V. Kuncak, I. Kuraj, and R. Piskac. Complete completion using types and weights. In PLDI, pages 27--38, 2013. Google ScholarDigital Library
- M. Hofmann. IgorII - an analytical inductive functional programming system (tool demo). In PEPM, pages 29--32, 2010. Google ScholarDigital Library
- D. Jackson. Structuring Z specifications with views. ACM Trans. Softw. Eng. Methodol., 4 (4): 365--389, 1995. Google ScholarDigital Library
- S. Jacobs, V. Kuncak, and P. Suter. Reductions for synthesis procedures. In VMCAI, pages 88--107, 2013.Google ScholarDigital Library
- J. Jaffar and J.-L. Lassez. Constraint logic programming. In POPL, pages 111--119, 1987. Google ScholarDigital Library
- B. Jobstmann and R. Bloem. Optimizations for LTL synthesis. In FMCAD, pages 117--124, 2006. Google ScholarDigital Library
- J. R. Josephson. Abductive Inference: Computation, Philosophy, Technology. Cambridge University Press, 1994.Google Scholar
- A. C. Kakas, R. A. Kowalski, and F. Toni. Abductive logic programming. J. Log. Comput., 2 (6): 719--770, 1992.Google ScholarCross Ref
- E. Kitzelmann and U. Schmid. Inductive synthesis of functional programs: An explanation based generalization approach. JMLR, 7: 429--454, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. S. Köksal, V. Kuncak, and P. Suter. Constraints as control. In POPL, pages 151--164, 2012. Google ScholarDigital Library
- V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Complete functional synthesis. In PLDI, pages 316--329, 2010. Google ScholarDigital Library
- V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Software synthesis procedures. CACM, 55 (2): 103--111, 2012. Google ScholarDigital Library
- V. Kuncak, E. Kneuss, and P. Suter. Executing specifications using synthesis and constraint solving (invited talk). In Runtime Verification (RV), 2013.Google ScholarCross Ref
- I. Kuraj. Interactive code generation. Master's thesis, EPFL, 02 2013.Google Scholar
- D. Leinenbach and T. Santen. Verifying the Microsoft Hyper-V hypervisor with VCC. In FM, pages 806--809, 2009. Google ScholarDigital Library
- Y. Lustig and M. Y. Vardi. Synthesis from component libraries. In FOSSACS, pages 395--409, 2009. Google ScholarDigital Library
- Z. Manna and R. J. Waldinger. Toward automatic program synthesis. Commun. ACM, 14 (3): 151--165, 1971. Google ScholarDigital Library
- Z. Manna and R. J. Waldinger. A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst., 2 (1): 90--121, 1980. Google ScholarDigital Library
- A. Martelli and U. Montanari. Additive AND/OR graphs. In IJCAI, pages 1--11, 1973. Google ScholarDigital Library
- S. Muggleton and L. D. Raedt. Inductive logic programming: Theory and methods. J. Log. Program., 19/20: 629--679, 1994.Google ScholarCross Ref
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002. Google ScholarDigital Library
- C. Okasaki. Purely functional data structures. Cambridge University Press, 1999. Google ScholarDigital Library
- Y. Pei, Y. Wei, C. A. Furia, M. Nordio, and B. Meyer. Code-based automated program fixing. ArXiv e-prints, 2011. arXiv:1102.1059. Google ScholarDigital Library
- N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In VMCAI, pages 364--380, 2006. Google ScholarDigital Library
- A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, 1989. Google ScholarDigital Library
- R. Singh and S. Gulwani. Synthesizing number transformations from input-output examples. In CAV, pages 634--651, 2012. Google ScholarDigital Library
- D. R. Smith. Generating programs plus proofs by refinement. In VSTTE, pages 182--188, 2005.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Solar-Lezama, C. G. Jones, and R. Bodík. Sketching concurrent data structures. In PLDI, pages 136--148, 2008. Google ScholarDigital Library
- A. Spielmann, A. Nötzli, C. Koch, V. Kuncak, and Y. Klonatos. Automatic synthesis of out-of-core algorithms. In SIGMOD, 2013. Google ScholarDigital Library
- S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In POPL, pages 313--326, 2010. Google ScholarDigital Library
- P. D. Summers. A methodology for LISP program construction from examples. JACM, 24 (1): 161--175, 1977. Google ScholarDigital Library
- P. Suter. Programming with Specifications. PhD thesis, EPFL, December 2012.Google Scholar
- P. Suter, M. Dotta, and V. Kuncak. Decision procedures for algebraic data types with abstractions. In POPL, pages 199--210, 2010. Google ScholarDigital Library
- P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive programs. In SAS, pages 298--315, 2011. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. T. Vechev, E. Yahav, and G. Yorsh. Inferring synchronization under limited observability. In TACAS, pages 139--154, 2009. Google ScholarDigital Library
- C. von Essen and B. Jobstmann. Program repair without regret. In CAV, pages 896--911, 2013. Google ScholarDigital Library
- Y. Wei, C. A. Furia, N. Kazmin, and B. Meyer. Inferring better contracts. In ICSE, pages 191--200, 2011. Google ScholarDigital Library
- N. Wirth. Program development by stepwise refinement. Commun. ACM, 14 (4): 221--227, 1971. Google ScholarDigital Library
Index Terms
- Synthesis modulo recursive functions
Recommendations
Synthesis modulo recursive functions
OOPSLA '13We 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 ...
Verification modulo theories
AbstractIn this paper, we consider the problem of model checking fair transition systems expressed symbolically in the framework of Satisfiability Modulo Theories. This problem, referred to as Verification Modulo Theories, is tackled by combining two key ...
Comments