Colloquium - Swarat Chaudhuri

I will speak about Cauchy, a long-term research project aiming to build formal methods, programming abstractions, and language implementations for uncertain and approximate computation (in the present talk, I restrict myself to the program analysis aspects). As we enter an era where computation is tightly intertwined with the physical world and deployed on resource-constrained devices, more and more programs operate in uncertain environments. As the costs of computational resources become more explicit and software with "soft" correctness requirements emerge, opportunities for approximate computing are also on the rise.

These trends raise several questions of interest to formal methods: How do we verify the correctness of programs in the presence of uncertainty?

How do we specify "soft" correctness requirements for programs, and how do we reason with respect to them?  Can we compile programs into forms that consume fewer resources but are yet approximately correct? The Cauchy project addresses all these questions and more. From results so far, it raises the possibility of a foundationally deep marriage between program verification and mathematical analysis, and opens up new applications of numerical optimization and machine learning in program analysis.