Much of my research explores the interplay between the deductive and algorithmic approaches to verification. As program verification is undecidable in general, the aim is to construct verification methods that work well in practice. A study of successful deductive proofs can suggest corresponding automated methods that are likely to work well. Conversely, the correctness of an implementation of a complex verification method can be established by generating an easily-checkable proof that justifies its conclusions.
I graduated with a B.Tech degree from IIT Madras and a Ph.D. from the University of Texas at Austin , with E. Allen Emerson as my thesis advisor. I then joined the Computing Sciences Research Center at Bell Labs (famously known as "Center 1127"), and have been here since. As a graduate student at UT Austin, I had the great good fortune to interact 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.