Swarat Chaudhuri

Computer Science and Engineering

Pennsylvania State University

Cauchy: Towards an analytical calculus of computation

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).