Swarat Chaudhuri

Pennsylvania State University

I will speak about Cauchy, a long-term research project aiming to build an "analytical calculus of computation": a system of mechanized reasoning about programs that can verify analytic program properties like continuity and smoothness, and compute analytic program attributes such as derivatives, discontinuities, limits, and smooth approximations.

 

The practical motivation of the project is to develop a new class of program analyses for an era where computing is intertwined with sensor-derived perceptions of the physical world, and correctness is a continuum rather than a boolean fact. For example, the desktop application of yesterday that runs on the cyber-physical system of today is still written in a standard language allowing branches, loops, 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.

 

We may now require that the program be "robust" to small measurement errors 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 ask that the program encode 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 tune real-valued program parameters, we may now want to use classical root-finding techniques, which may only work on an analytic approximation of the program. To argue that the program converges, we may want to compute limits on its outputs as time elapses to infinity. Common to the above scenarios is the need for some form of analytic reasoning about programs.

 

The scope of Cauchy includes the theoretical foundations of such reasoning, ways to automate it using state-of-the-art constraint-solvers and numerical optimizers, and the applications of the resultant tools in program verification, synthesis, optimization, and approximation. In the recently-published first paper out of this project, we have given a method to automatically verify that the observable behavior of a program is continuous. In a subsequent paper, we give a method to compute smooth approximations of programs and apply it to the synthesis of control parameters of cyber-physical systems. From evidence so far, Cauchy opens up a new playground for research on reasoning about programs. It also raises the possibility of a fruitful union of program semantics and verification with control theory, numerical analysis, machine learning, and computer algebra.

4:15pm

B17 Upson Hall

Tuesday, April 13, 2010

Refreshments at 3:45pm in the Upson 4th Floor Atrium

 

Computer Science

Colloquium

Spring 2010

www.cs.cornell.edu/events/colloquium

Cauchy:

Towards an analytical calculus of computation