Colloquium Details
Cauchy: Towards an Analytical Calculus of Computation
Speaker: Swarat Chaudhuri, Pennsylvania State University
Location: Warren Weaver Hall 1302
Date: March 29, 2010, 11:30 a.m.
Host: Richard Cole
Synopsis:
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.
Speaker Bio:
Swarat Chaudhuri is an assistant professor of Computer Science and Engineering at Pennsylvania State University. 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 in 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 Ph.D. 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 for the best computer science dissertation from the University of Pennsylvania.
Notes:
In-person attendance only available to those with active NYU ID cards.