From boolean to quantitative synthesis

12 years 4 months ago

Download pub.ist.ac.at

Motivated by improvements in constraint-solving technology and by the increase of routinely available computational power, partial-program synthesis is emerging as an eﬀective 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 satisﬁes the speciﬁcation. As an example, consider a partial program where threads access shared data without using any synchronization mechanism, and a declarative speciﬁcation 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 speciﬁcation. In this paper, we argue that quantitative objectives are needed in partial-program synthesis in order to produce higher-qualit...

Pavol Cerný, Thomas A. Henzinger

Real-time Traffic