An Update on Deductive Synthesis and Repair in the Leon Tool

Manos Koukoutos
(EPFL)
Etienne Kneuss
(EPFL)
Viktor Kuncak
(EPFL)

We report our progress in scaling deductive synthesis and repair of recursive functional Scala programs in the Leon tool. We describe new techniques, including a more precise mechanism for encoding the space of meaningful candidate programs. Our techniques increase the scope of synthesis by expanding the space of programs we can synthesize and by reducing the synthesis time in many cases. As a new example, we present a run-length encoding function for a list of values, which Leon can now automatically synthesize from specification consisting of the decoding function and the local minimality property of the encoded value.

In Ruzica Piskac and Rayna Dimitrova: Proceedings Fifth Workshop on Synthesis (SYNT 2016), Toronto, Canada, July 17-18, 2016, Electronic Proceedings in Theoretical Computer Science 229, pp. 100–111.
Published: 22nd November 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.229.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org