Swarat Chaudhuri
Location: (University Park, PA)
Personal Research Web Page: http://www.cse.psu.edu/~swarat
Keywords: Program analysis, Verification, Automated reasoning, Semantics, Mathematical analysis, Continuity, Calculus
Posted on: Monday, May 10th, 2010
Broad Research Area: Programming Languages / Compilers, Software Engineering, Theory / Algorithms
Research Interests:
I am broadly interested in formal, automated methods for program verification and synthesis, in particular abstract interpretation and model checking. I am also broadly interested in languages, models, and systems for parallel programming.
I am seeking a postdoctoral researcher to work with me on Cauchy, a long-term project aiming to build an “analytical calculus of computation”: a system of mechanized reasoning that can verify whether a program satisfies “analytic” properties like continuity and smoothness, and compute derivatives, discontinuities, limits, and other analytic attributes of programs. 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, we may now require that the program be “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 ask that the program encode a continuous function over this space. Alternately, we may consider the Lipschitz constant of the program as a measure of its robustness. To tune program parameters, we may want to use classical root-finding techniques, which may only work on an analytic approximation of the program. To argue that a 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 its applications in program verification, synthesis, optimization, and approximation. From evidence so far, Cauchy opens 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.
Contact Information:
Please email me at the email address provided above.
