Automated Software Synthesis.

Researchers at EPFL discovered a new method to automatically generate computer software components that are guaranteed to behave correctly. Among the benefits of this line of research is making software development easier and making our computing infrastructure less vulnerable to crashes and hangs.

Automated software synthesis from specifications reduces the effort needed to obtain the results, because the user only needs to indicate what needs to achieved, not how. It also increases the confidence in the correctness of results, since the generated program is guaranteed to satisfy the indicated properties for all possible program inputs. The key insight in this work was to develop algorithms for solving logical specifications with parameters, generalizing ideas such as those used to solve systems of equations. The resulting algorithm can be used to automatically compile certain classes of declarative specifications into executable code.

"I predict that as we identify more such restricted languages and integrate them into general-purpose (Turing-complete) languages, we will make programming more productive and programs more reliable.", writes in his technical perspective Rastislav Bodik, Associate Professor at the University of California, Berkeley.

The techniques are being integrated into the compiler for the programming language Scala developed in the research group of Professor Martin Odersky and commercially supported by the Typesafe startup of EPFL.

This work is part of a broader research agenda in the EPFL Laboratory for Automated Reasoning and Analysis (LARA), led by Viktor Kuncak, Assistant Professor in the School of Computer and Communication Sciences. The overall goal is to automatically synthesize computer systems from human intentions. Beyond ensuring the absence of errors and improved productivity, this work can lead to increasing our confidence in the scientific discoveries derived using computers, as well as unleashing the creative potentials of non-expert computer users.

The research, authored by Viktor Kuncak, Mikael Mayer, Philippe Suter, and Ruzica Piskac, was published in the International ACM Conference on Programming Language and Design and Implementation (PLDI), the Springer Journal of Software Tools for Technology Transfer (STTT), and the Research Highlights section of the Communications of the ACM (February 2012 issue). Communications of the ACM has recently been reorganized along the lines of Science or Nature, with top-quality research content as a major component. The Research Highlights section is devoted to the most important research results published in CS in recent years.

For more information: http://lara.epfl.ch/w/impro