Abstract
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesis over unbounded domains. Comfusy accepts expressions with input and output variables specifying relations on integers and sets. Comfusy symbolically computes the precise domain for the given relation and generates the function from inputs to outputs. The outputs are guaranteed to satisfy the relation whenever the inputs belong to the relation domain. The core of our synthesis algorithm is an extension of quantifier elimination that generates programs to compute witnesses for eliminated variables. We present examples that demonstrate software synthesis using Comfusy and illustrate how synthesis simplifies software development.
Chapter PDF
Similar content being viewed by others
References
Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.Ā 4590, pp. 258ā262. Springer, Heidelberg (2007)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: ACM Conf. Programming Language Design and Implementation, PLDI (2010)
Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated ReasoningĀ 36(3), 213ā239 (2006)
Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. Communications of the ACMĀ 14(3), 151ā165 (1971)
de Moura, L., BjĆørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.Ā 4963, pp. 337ā340. Springer, Heidelberg (2008)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symp. Principles of Programming Languages, POPL (1989)
Pugh, W.: A practical algorithm for exact array dependence analysis. Communications of the ACMĀ 35(8), 102ā114 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
Ā© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kuncak, V., Mayer, M., Piskac, R., Suter, P. (2010). Comfusy: A Tool for Complete Functional Synthesis. In: Touili, T., Cook, B., Jackson, P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14295-6_38
Download citation
DOI: https://doi.org/10.1007/978-3-642-14295-6_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14294-9
Online ISBN: 978-3-642-14295-6
eBook Packages: Computer ScienceComputer Science (R0)