I work in computer science at Bell Labs.
My research is on methods that simplify the creation of provably correct and secure programs.
#### Contact

E-mail: kedar.namjoshi AT nokia-bell-labs.com

Phone: (+1) 908.582.1891

Address: Room 2B-435, 600-700 Mountain Avenue, Murray Hill, NJ 07974, USA

Phone: (+1) 908.582.1891

Address: Room 2B-435, 600-700 Mountain Avenue, Murray Hill, NJ 07974, USA

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.

Contributions include

- Decidability of Parameterized Verification, based on cutoff theorems
- Well-Founded Bisimulation, which considerably simplifies proofs of program equivalence under stuttering
- Establishing strong linkages between deductive proofs and abstraction methods (Deductive Proof = Abstraction; Model Checking)
- Algorithms for compositional (i.e., "bits and pieces") analysis of concurrent programs
- Using local (i.e., "neighborhood") symmetries to reduce the complexity of compositional verification
- Verifying sophisticated compiler optimizations with a proof-generating strategy called "witnessing"

- Establishing the correctness and security of compiler optimizations
- The use of local symmetry arguments in decision procedures for parameterized compositional model checking
- The synthesis of privacy-preserving and failure-tolerant programs from specifications

And an up-to-date list of publications; the full list is on DBLP .

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 (better 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.