University of Pennsylvania - PRECISE

Mechanized, logical approaches to reasoning about programs have often been collectively called the calculus of computation. Unlike the calculus of the physical sciences, the calculus of computation has not historically been concerned with "analytic" properties like continuity and smoothness. The traditional argument for this is that programs are discontinuous creatures, and that when continuous dynamics do arise, they can be abstractly modeled using differential equations and analyzed using the other calculus.

This argument, however, feels harder to justify as we enter an era where computing is intertwined with sensor-derived perceptions of the physical world, and correctness is often a continuum than a 0-1 fact. The desktop application of yesterday that runs on the cyber-physical system of today is still written in a standard programming language allowing branches, loops, queues, and arrays, and must still satisfy traditional safety and liveness properties. However, as it now processes real-valued, real-time satellite and sensor data, it must also offer a new set of guarantees that were traditionally applicable to continuous settings. For example, we may now require that the program is "robust" to small amounts of uncertainty in its inputs---i.e., that small perturbations to an input state only lead to small changes to the output state. A way to formalize this statement would be to define a metric space over the states of the program, and asking that the program encodes a continuous function over this space. Alternately, we may consider the derivative of the program as a measure of its robustness, insisting that a program with a smaller derivative is more robust. To make a non-robust program robust, we may want to replace it by an analytic approximation. To argue about the convergence of a program, we may want to compute limits on its outputs as time elapses to infinity.

A calculus of computation that can reason about "analytic" properties of programs would thus seem to have some clear practical applications. The goal of the Cauchy research project is to devise such a calculus, automate it using state-of-the-art constraint-solvers and numerical optimizers, and apply it in program verification, synthesis, optimization, and approximation. In the recently-published first paper out of this project, we give a method to syntactically verify that a program represents a continuous function. In a subsequent paper, we give a method to compute smooth approximations of programs and apply it to program synthesis. From evidence so far, Cauchy opens a new frontier for research on reasoning about programs. It also raises the possibility of a lasting marriage between program semantics and verification on one hand, and computer algebra, numerical analysis, and machine learning on the other.

Swarat Chaudhuri has been an assistant professor of Computer Science and Engineering at the Pennsylvania State University, University Park, since January 2008. He is an expert on formal, automated methods for program verification and synthesis, in particular abstract interpretation and model checking. His other main interest is languages, models, and systems for parallel programming.

Swarat received a bachelor's degree in computer science from the Indian Institute of Technology, Kharagpur, in 2001, and a doctoral degree in computer science from the University of Pennsylvania in 2007. He is a recipient of the National Science Foundation CAREER award, the ACM SIGPLAN Outstanding Doctoral Dissertation Award, and the Morris and Dorothy Rubinoff Award (awarded to the outstanding computer science dissertation from the University of Pennsylvania).