Developing correct and secure software is challenging. My research is on methods that simplify the construction of such programs, and provide mathematical guarantees of their correctness and security.
Much of this research is driven by the fascinating interplay between deductive and algorithmic approaches to program correctness. Deductive methods can suggest new automated approaches (e.g., for compositional reasoning). Conversely, algorithmic methods can be fruitfully viewed as proof generators (e.g. certifying automated model checkers).
My research includes work on
- Parameterized verification: Cutoff theorems which show that one can establish correctness of protocols for arbitrarily large network sizes by analyzing a few small instances, up to the cutoff bound.
- Program equivalence: A well-founded bisimulation proof method that considerably simplifies proofs of program equivalence, e.g., for pipeline processors and compiler optimizations.
- Abstraction principles: Linkages between deductive proofs, model checking and abstraction, and their use for fast, incremental program verification.
- Compositional reasoning: Fixed point methods for compositional (i.e., divide-and-conquer) analysis of large concurrent programs, and neighborhood symmetry principles which further simplify this analysis and provide broadly applicable parameterized cutoffs.
- Self-certification: Ensuring the correctness of of complex software -- model checkers, optimizing compilers and network OS's -- through generated proof certificates.
- Program Synthesis: Automatically generating programs from abstract specifications of their behavior; in particular, programs that work under adversarial conditions.
This research has been supported, in part, by grants from the NSF and DARPA.
And a bit more ...
Here is my academic CV
And an up-to-date list of publications; the full list is on DBLP .
I had the privilege of presenting a talk on the history of computing at Bell Labs at the IEEE Milestone dedication ceremony in December 2014.
I graduated with a B.Tech degree from IIT Madras and a Ph.D. from the University of Texas at Austin, where E. Allen Emerson was my
thesis advisor. I then joined the Computing Sciences Research Center at
Bell Labs (better known as Center 1127), and have been here since. As a graduate student at UT Austin, I had the good fortune to interact closely with Edsger W. Dijkstra, as a member of the ATAC (Dijkstra's Austin Tuesday Afternoon Club). His views on what constitutes good research and the example he put forward have had a deep and long-lasting influence.