An Update on Deductive Synthesis and Repair in the Leon Tool

An Update on Deductive Synthesis and Repair in the Leon Tool

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 expandin...

Full description

Bibliographic Details
Main Authors: Manos Koukoutos, Etienne Kneuss, Viktor Kuncak
Format: Article
Language:English
Published: Open Publishing Association 2016-11-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1611.07625v1
id doaj-9ceb2770e0f34ff2a75c31af6493c874
record_format Article
spelling doaj-9ceb2770e0f34ff2a75c31af6493c8742020-11-24T22:38:53ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-11-01229Proc. SYNT 201610011110.4204/EPTCS.229.9:9An Update on Deductive Synthesis and Repair in the Leon ToolManos Koukoutos0Etienne Kneuss1Viktor Kuncak2 EPFL EPFL 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.http://arxiv.org/pdf/1611.07625v1
collection DOAJ
language English
format Article
sources DOAJ
author Manos Koukoutos
Etienne Kneuss
Viktor Kuncak
spellingShingle Manos Koukoutos
Etienne Kneuss
Viktor Kuncak
An Update on Deductive Synthesis and Repair in the Leon Tool
Electronic Proceedings in Theoretical Computer Science
author_facet Manos Koukoutos
Etienne Kneuss
Viktor Kuncak
author_sort Manos Koukoutos
title An Update on Deductive Synthesis and Repair in the Leon Tool
title_short An Update on Deductive Synthesis and Repair in the Leon Tool
title_full An Update on Deductive Synthesis and Repair in the Leon Tool
title_fullStr An Update on Deductive Synthesis and Repair in the Leon Tool
title_full_unstemmed An Update on Deductive Synthesis and Repair in the Leon Tool
title_sort update on deductive synthesis and repair in the leon tool
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2016-11-01
description 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.
url http://arxiv.org/pdf/1611.07625v1
work_keys_str_mv AT manoskoukoutos anupdateondeductivesynthesisandrepairintheleontool
AT etiennekneuss anupdateondeductivesynthesisandrepairintheleontool
AT viktorkuncak anupdateondeductivesynthesisandrepairintheleontool
AT manoskoukoutos updateondeductivesynthesisandrepairintheleontool
AT etiennekneuss updateondeductivesynthesisandrepairintheleontool
AT viktorkuncak updateondeductivesynthesisandrepairintheleontool
_version_ 1725711251865075712

Similar Items