---

Producing good software is challenging. My research develops methods to simplify program construction while providing precise guarantees of correctness and security.

Much of my research is driven by a fascinating interplay between the deductive and algorithmic approaches to program verification. Deductive methods formalize intuitive patterns of reasoning. Those patterns can be automated and used to guide correct program construction. Conversely, algorithmic methods such as model checking can be modified to generate deductive proofs that justify their results.

Research Highlights

• Parameterized Protocol Verification: Cutoff theorems make it possible to show that a protocol is correct for all configurations by checking only a few small instances.

• Program Equivalence: Well-founded bisimulations simplify proofs of equivalence between programs, which is useful for establishing the correctness of pipelined machines and optimizing compilers.

• Abstraction: Linkages between deductive proofs, model checking, and abstraction lead to fast, incremental program analysis.

• Modular Reasoning: Divide-and-conquer methods tackle state explosion in the analysis of large concurrent programs, while new symmetry principles further speed up modular analysis.

• Self-Certification: Run-time certificates formally guarantee the correctness of complex software -- model checkers, optimizing compilers, and network OS's.

• Synthesis: Automatically generated programs coordinate groups of software agents, guiding them towards a desired joint behavior.

This research has been supported, in part, by grants from the NSF and DARPA.

---

And a bit more...

I was recently named an ACM Distinguished Member (class of 2022).

My CV and an up-to-date list of publications; the full list is on DBLP .

I had the privilege of giving a talk on the history of computing at Bell Labs at an IEEE Milestone dedication ceremony at Murray Hill 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 famed Computing Sciences Research Center at Bell Labs (perhaps 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 his ATAC (the Austin Tuesday Afternoon Club). His views on what constitutes good research and good writing and the example that he put forward have had a deep and long-lasting influence.