An Update on Deductive Synthesis and Repair in the Leon Tool

TL;DR

This paper discusses advancements in the Leon tool that enhance deductive synthesis and repair of recursive Scala programs, enabling more efficient and broader program synthesis through new encoding techniques and demonstrating with a run-length encoding example.

Contribution

The paper introduces a more precise encoding mechanism for candidate programs, expanding the synthesis scope and reducing synthesis time in the Leon tool.

Findings

Increased synthesis scope for recursive Scala programs

Reduced synthesis time with new encoding techniques

Successfully synthesized run-length encoding function from specifications

Abstract

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.