Abstract
A synthesis procedure acts as a compiler for declarative specifications. It accepts a formula describing a relation between inputs and outputs, and generates a function implementing this relation. This paper presents the first synthesis procedures for 1) algebraic data types and 2) arrays. Our procedures are reductions that lift a synthesis procedure for the elements into synthesis procedures for containers storing these elements. We introduce a framework to describe synthesis procedures as systematic applications of inference rules. We show that, by interpreting both synthesis problems and programs as relations, we can derive and modularly prove widely applicable transformation rules, simplifying both the presentation and the correctness argument.
Swen Jacobs was supported in part by the European Commission through project DIAMOND (FP7-2009-IST-4-248613), the Austrian Science Fund (FWF) through the national research network RiSE (S11406), the Swiss NSF Grant 200021_132176, and COST Action IC0901. Philippe Suter was supported in part by the Swiss NSF Grant 200021_120433.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aït-Kaci, H.: Warren’s Abstract Machine: A Tutorial Reconstruction. MIT Press (1991) (available online as PDF)
Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning. Elsevier (2001)
Flener, P.: Logic Program Synthesis from Incomplete Information. Kluwer Academic Publishers (1995)
Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: FMCAD, pp. 101–109 (2010)
Hodges, W.: A Shorter Model Theory. Cambridge University Press (1997)
Jobstmann, B., Bloem, R.: Optimizations for ltl synthesis. In: FMCAD, pp. 117–124 (2006)
Köksal, A.S., Kuncak, V., Suter, P.: Constraints as control. In: POPL, pp. 151–164 (2012)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. CACM 55(2), 103–111 (2012)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI, pp. 316–329 (2010)
Lahiri, S.K., Ball, T., Cook, B.: Predicate Abstraction via Symbolic Decision Procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 24–38. Springer, Heidelberg (2005)
Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. CACM 14(3), 151–165 (1971)
Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. TOPLAS 2(1), 90–121 (1980)
Maranget, L.: Compiling pattern matching to good decision trees. In: ML, pp. 35–46 (2008)
de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45–52 (2009)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245–257 (1979)
Smith, D.R.: KIDS: A semiautomatic program development system. TSE 16(9), 1024–1043 (1990)
Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404–415 (2006)
Spielmann, A., Kuncak, V.: Synthesis for unbounded bit-vector arithmetic. In: IJCAR, pp. 499–513 (2012)
Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313–326 (2010)
Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS, pp. 29–37 (2001)
Sturm, T., Weispfenning, V.: Quantifier elimination in term algebras: The case of finite languages. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing (CASC). TUM München (2002)
Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL, pp. 327–338 (2010)
Wadler, P.: The Implementation of Functional Programming Languages: Efficient Compilation of Pattern-matching, ch. 5, pp. 78–103 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacobs, S., Kuncak, V., Suter, P. (2013). Reductions for Synthesis Procedures. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2013. Lecture Notes in Computer Science, vol 7737. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35873-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-35873-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35872-2
Online ISBN: 978-3-642-35873-9
eBook Packages: Computer ScienceComputer Science (R0)