From boolean to quantitative synthesis

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

• Type: Journal
• Year: 2011
• Where: EMSOFT
• Authors: Pavol Cerný, Thomas A. Henzinger
• Keywords: EMSOFT 2011, Engineering Design Tools, Software Engineering, Software Engineering Design, Software Engineering Metrics