
- Ph.D., Univ. of California, Berkeley, 1990
- M.S., Computer Science, Univ. of California, Berkeley, 1987
- B.Tech., Electrical Engineering, Indian Institute of Technology, New Delhi, 1985
I am broadly interested in designing computing systems that are functionally correct and secure. My work combines system design with mathematical modeling and analysis techniques for proving functional correctness and security properties for these systems. We do this through studying new modeling techniques as well as algorithms for correctness proofs. Most recently my research has focused on developing the Instruction-Level Abstraction (ILA) model for scalable systems-on-chip design and verification. In the past my group has worked on efficient solvers for Boolean Satisfiability problems (SAT and MAX-SAT) which are fundamental techniques used in system verification and other applications.
I am also open to advising projects where the ideas are initiated by students - these could involve hardware, software or theory - I am very open!
-
“Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification,” (with B-Y. Huang, H. Zhang, P. Subramanyan, Y. Vizel, and A. Gupta), ACM Transactions on Design Automation of Electronic Systems (TODAES), 24(1): 10:1-10:24 (2019)
-
“ Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification,” with H. Zhang, C. Trippel, Y Manerkar, A. Gupta, and M Martonosi, Formal Methods in Computer-Aided Design (FMCAD), 2018
-
Propositional SAT Solving, in Handbook of Model Checking (with J. Marques-Silva) 2018: 247-275
-
“Reverse Engineering Digital Circuits Using Structural and Functional Analyses,” (with P. Subramanyan, N. Tsiskaridze, W. Li, A. Gascon, W. Y. Tan, A. Tiwari, N. Shankar, S. Seshia), IEEE Transactions on Emerging Topics in Computing, vol.2, no.1, pp.63-80, March 2014
-
“Boolean Satisfiability: From Theoretical Hardness to Practical Success,” (with L. Zhang), Invited Paper, Communications of the ACM, Volume 52, Number 8, August 2009
Honors and Awards:
- Intel Corporate Research Council Outstanding Researcher Award (Security and Software Sector), 2018
- IEEE CEDA A. Richard Newton Technical Impact Award in Electronic Design Automation, 2017
- The IEEE/ACM Design Automation Conference 50th Anniversary Most Cited Paper Award: (with M. W. Moskewicz, C. F. Madigan, Y. Zhao and L. Zhang) For publishing the most cited paper in DAC's 50 year history, 2013
- IEEE/ACM International Conference on Computer-Aided Design, Ten Year Retrospective Most Influential Paper Award, 2011
- Computer-Aided Verification (CAV) Award for fundamental contributions to the development of high-performance Boolean satisfiability solvers, 2009
- Princeton University President’s Award for Distinguished Teaching, 2009