Composing Composure: Reasoning about Robustness of Software Systems

Most software is inherently nonrobust--change the operating conditions of a typical program slightly, and you may obtain very different results. This lack of robustness can not only result in unpredictable runtime behavior, it also makes testing, approximation, and mathematical analysis of programs highly challenging.

We will argue that methods for automated logical reasoning about programs provide a way to cope with this problem. Using a program analysis, we can sometimes determine if a given program is robust, and if so, exploit this property. On the other hand, if a program is not robust, logic can help us approximate it into one that is robust. Using applications from several different areas of computer science, I will show how these techniques can lead to more reliable program execution under uncertainty, opportunities for language-based approximate computation, and easier solutions to hard optimization problems involving programs.

Swarat Chaudhuri is an Assistant Professor of Computer Science at Rice University. His research lies in the interface of automated reasoning and programming languages.