home · mobile · calendar · colloquia · 2011-2012 · 

Colloquium - Cerny

From Boolean to Quantitative Synthesis
IST Austria

Computer-aided programming, or partial-program synthesis, is emerging as an effective approach for increasing programmer productivity. Its goal is to harness the improvements in constraint-solving technology and the increase in routinely available computational power to enable the programmer to specify a part of her intent imperatively (that is, to give a partial program) and a part of her intent declaratively, by specifying which conditions need to be achieved or maintained. An important instance of this approach is the synthesis of synchronization, where on one hand it is often easier to specify the intended sequential behavior of threads imperatively, and on the other hand, it is often easier to specify synchronization conditions declaratively, by for example requiring the absence of data races and deadlocks.

We advance the thesis that quantitative measures are needed in partial-program synthesis in order to produce higher-quality programs, while enabling simpler specifications. In synthesis of synchronization, the synthesizer could construct a naive solution that uses one global lock for all 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 defining a quantitative objective that models performance. Other quantitative notions useful in synthesis include fault tolerance, robustness, resource consumption, and information flow.

Pavol Cerny is a postdoctoral researcher at IST Austria. He obtained his PhD in Computer Science from the University of Pennsylvania in 2009 and a DEA diploma from École normale supérieure, Paris, France in 2003. His research interests are in formal methods and programming languages, in particular in quantitative program synthesis and in algorithmic verification of concurrent software.

Sponsored by the Department of Electrical, Computer and Energy Engineering.

Department of Computer Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
May 5, 2012 (14:13)