From boolean to quantitative synthesis

P. Cerny, T.A. Henzinger, in:, ACM, 2011, pp. 149–154.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published | English
Department
Abstract
Motivated by improvements in constraint-solving technology and by the increase of routinely available computational power, partial-program synthesis is emerging as an effective approach for increasing programmer productivity. The goal of the approach is to allow the programmer to specify a part of her intent imperatively (that is, give a partial program) and a part of her intent declaratively, by specifying which conditions need to be achieved or maintained. The task of the synthesizer is to construct a program that satisfies the specification. As an example, consider a partial program where threads access shared data without using any synchronization mechanism, and a declarative specification that excludes data races and deadlocks. The task of the synthesizer is then to place locks into the program code in order for the program to meet the specification. In this paper, we argue that quantitative objectives are needed in partial-program synthesis in order to produce higher-quality programs, while enabling simpler specifications. Returning to the example, the synthesizer could construct a naive solution that uses one global lock for shared data. This can be prevented either by constraining the solution space further (which is error-prone and partly defeats the point of synthesis), or by optimizing a quantitative objective that models performance. Other quantitative notions useful in synthesis include fault tolerance, robustness, resource (memory, power) consumption, and information flow.
Publishing Year
Date Published
2011-10-09
Acknowledgement
This work was partially supported by the ERC Advanced Grant QUAREM, the FWF NFN Grant S11402-N23 (RiSE), and the EU NOE Grant ArtistDesign.
Page
149 - 154
Conference
EMSOFT: Embedded Software
Conference Location
Taipei; Taiwan
Conference Date
2011-10-09 – 2011-10-14
IST-REx-ID

Cite this

Cerny P, Henzinger TA. From boolean to quantitative synthesis. In: ACM; 2011:149-154. doi:10.1145/2038642.2038666
Cerny, P., & Henzinger, T. A. (2011). From boolean to quantitative synthesis (pp. 149–154). Presented at the EMSOFT: Embedded Software , Taipei; Taiwan: ACM. https://doi.org/10.1145/2038642.2038666
Cerny, Pavol, and Thomas A Henzinger. “From Boolean to Quantitative Synthesis,” 149–54. ACM, 2011. https://doi.org/10.1145/2038642.2038666.
P. Cerny and T. A. Henzinger, “From boolean to quantitative synthesis,” presented at the EMSOFT: Embedded Software , Taipei; Taiwan, 2011, pp. 149–154.
Cerny P, Henzinger TA. 2011. From boolean to quantitative synthesis. EMSOFT: Embedded Software 149–154.
Cerny, Pavol, and Thomas A. Henzinger. From Boolean to Quantitative Synthesis. ACM, 2011, pp. 149–54, doi:10.1145/2038642.2038666.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar