skip to main content
Department of Computer Science University of Colorado Boulder
cu: home | engineering | mycuinfo | about | cu a-z | search cu | contact cu cs: about | calendar | directory | catalog | schedules | mobile | contact cs
home · events · colloquia · 2011-2012 · 

Colloquium - Cerny

ECCR 265

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.

The Department holds colloquia throughout the Fall and Spring semesters. These colloquia, open to the public, are typically held on Thursday afternoons, but sometimes occur at other times as well. If you would like to receive email notification of upcoming colloquia, subscribe to our Colloquia Mailing List. If you would like to schedule a colloquium, see Colloquium Scheduling.

Sign language interpreters are available upon request. Please contact Stephanie Morris at least five days prior to the colloquium.

See also:
Department of Computer Science
College of Engineering and Applied Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
Send email to

Engineering Center Office Tower
ECOT 717
FAX +1-303-492-2844
XHTML 1.0/CSS2 ©2012 Regents of the University of Colorado
Privacy · Legal · Trademarks
May 5, 2012 (13:29)