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...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Springer Berlin Heidelberg
2017
|
| Online Access: | http://hdl.handle.net/1721.1/106200 https://orcid.org/0000-0001-7604-8252 |
| _version_ | 1811090204834922496 |
|---|---|
| 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 |