Program sketching
Sketching is a synthesis methodology that aims to bridge the gap between a programmer’s high-level insights about a problem and the computer’s ability to manage low-level details. In sketching, the programmer uses a partial program, a sketch, to describe the desired implementation strategy, and leav...
Hoofdauteur: | |
---|---|
Andere auteurs: | |
Formaat: | Artikel |
Taal: | English |
Gepubliceerd in: |
Springer Berlin Heidelberg
2017
|
Online toegang: | http://hdl.handle.net/1721.1/106200 https://orcid.org/0000-0001-7604-8252 |
_version_ | 1826209971657768960 |
---|---|
author | Solar Lezama, Armando |
author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Solar Lezama, Armando |
author_sort | Solar Lezama, Armando |
collection | MIT |
description | Sketching is a synthesis methodology that aims to bridge the gap between a programmer’s high-level insights about a problem and the computer’s ability to manage low-level details. In sketching, the programmer uses a partial program, a sketch, to describe the desired implementation strategy, and leaves the low-level details of the implementation to an automated synthesis procedure. In order to generate an implementation from the programmer provided sketch, the synthesizer uses counterexample-guided inductive synthesis (CEGIS). Inductive synthesis refers to the process of generating candidate implementations from concrete examples of correct or incorrect behavior. CEGIS combines a SAT-based inductive synthesizer with an automated validation procedure, a bounded model-checker, that checks whether the candidate implementation produced by inductive synthesis is indeed correct and to produce new counterexamples. The result is a synthesis procedure that is able to handle complex problems from a variety of domains including ciphers, scientific programs, and even concurrent data-structures. |
first_indexed | 2024-09-23T14:37:51Z |
format | Article |
id | mit-1721.1/106200 |
institution | Massachusetts Institute of Technology |
language | English |
last_indexed | 2024-09-23T14:37:51Z |
publishDate | 2017 |
publisher | Springer Berlin Heidelberg |
record_format | dspace |
spelling | mit-1721.1/1062002022-09-29T10:00:14Z Program sketching Solar Lezama, Armando Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Solar Lezama, Armando Sketching is a synthesis methodology that aims to bridge the gap between a programmer’s high-level insights about a problem and the computer’s ability to manage low-level details. In sketching, the programmer uses a partial program, a sketch, to describe the desired implementation strategy, and leaves the low-level details of the implementation to an automated synthesis procedure. In order to generate an implementation from the programmer provided sketch, the synthesizer uses counterexample-guided inductive synthesis (CEGIS). Inductive synthesis refers to the process of generating candidate implementations from concrete examples of correct or incorrect behavior. CEGIS combines a SAT-based inductive synthesizer with an automated validation procedure, a bounded model-checker, that checks whether the candidate implementation produced by inductive synthesis is indeed correct and to produce new counterexamples. The result is a synthesis procedure that is able to handle complex problems from a variety of domains including ciphers, scientific programs, and even concurrent data-structures. 2017-01-05T15:44:02Z 2017-01-05T15:44:02Z 2012-08 2016-08-18T15:28:46Z Article http://purl.org/eprint/type/JournalArticle 1433-2779 1433-2787 http://hdl.handle.net/1721.1/106200 Solar-Lezama, Armando. “Program Sketching.” International Journal on Software Tools for Technology Transfer 15.5–6 (2013): 475–495. https://orcid.org/0000-0001-7604-8252 en http://dx.doi.org/10.1007/s10009-012-0249-7 International Journal on Software Tools for Technology Transfer Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ Springer-Verlag application/pdf Springer Berlin Heidelberg Springer Berlin Heidelberg |
spellingShingle | Solar Lezama, Armando Program sketching |
title | Program sketching |
title_full | Program sketching |
title_fullStr | Program sketching |
title_full_unstemmed | Program sketching |
title_short | Program sketching |
title_sort | program sketching |
url | http://hdl.handle.net/1721.1/106200 https://orcid.org/0000-0001-7604-8252 |
work_keys_str_mv | AT solarlezamaarmando programsketching |