PhD, Carnegie Mellon University
Formal verification of software systems via SMT solvers, theorem provers, and learning state machines. Published at top CS conferences, 1700+ citations, h-index 23.
IBM Research — Architect, Cognitive Analytics (2011–2016)
Built an end-to-end conversational AI system for natural-language data analytics: speech-to-text, NLP query understanding, and multi-screen visualization.
NEC Labs — Research Engineer (2007–2011)
Formal verification of sequential and concurrent programs using symbolic reasoning, compiler analysis, and constraint solving.
10 years, independent consulting (2016–present)
Production AI search and retrieval systems for finance, e-commerce, telecom, and legal clients — from neural IR and hybrid search to agentic RAG pipelines for S&P 500 clients.