Swarat Chaudhuri

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

We will argue that the key to coping with this nonrobustness lies in the structure that is manifest in software systems. As engineered rather than natural objects, programs come with code that is amenable to logical analysis. I will show that using the toolbox of automated logical reasoning about programs, we can sometimes tell which programs are robust and which are not. Also, if a program is nonrobust, logic can help us approximate it into one that is not. Using applications from several different areas of computer science, I will show how these methods can lead to more predictable functioning and easier development of programs.