Nishant Sinha

Electrical and Computer Engineering
Carnegie Mellon University

off: 3703 Wean Hall, 5000 Forbes Ave, Pittsburgh PA 15213.
ph: 412-268-1718
nishant at cmu edu

I obtained my PhD in ECE, CMU working with Prof. Ed Clarke as my advisor. My CV.

I obtained an M.S. in Computer Engineering from ECE, CMU in 2003 and a B. Tech. (Hons.) in Computer Sc. and Engg. from IIT Kharagpur in 2001.

I defended my thesis on 24^th August 2007.

Now, I work as a Research Staff Member at NEC Labs, Princeton.

Research:

My thesis research focuses on formal methods for scalable software and hardware verification in general and across evolution.
Misc. keywords: Compositional Verification of Hardware and Concurrent Software, Automata Learning algorithms, Checking Component Substitutability, Decision Procedures.

Component Substitutability. Re-validating system-level, component-based, hardware and software systems across their evolution (e.g., upgrades, re-designs) is a major concern. As part of my thesis research, I have developed efficient techniques to re-validate such systems upon upgrades, which rely on automated abstraction and automated incremental compositional reasoning. My research is targeted towards the broader goal of correct-by-construction system design.

Symbolic Modular Analyzer. Automated compositional reasoning requires the availability of environment assumptions for system components. I have developed a SAT/SMT-based approach for automatically computing such assumptions for shared memory systems using lazy automata learning algorithms and model checking. The tool SYMODA (available here) implements this approach for hardware systems.

Concurrent Software Verification. My research also contributes to MAGIC/ComFoRT software verification framework for verifying concurrent message-passing programs based on automated counterexample-guided abstraction. In particular, we have developed automated compositional techniques for verifying existence of deadlocks and for checking simulation conformance for concurrent message-passing programs. I have also worked on SAT- and BDD-based symbolic partial order reduction techniques for analyzing asynchronous concurrent software systems.

Details of my research can be found in the publications on the research page.

Misc. Talks:

Thesis Defense (ppt), Aug 2007.
SAT-based Compositional Verification using Lazy Learning (ppt), CAV, July 2007.
Compositional Verification for System-on-Chip Designs (ppt), SRC Student Symposium, Oct 2006.
Best Paper in Session Award.
PhD Proposal: (ppt), Mar 2006.
Abstraction in Model Checking (ppt), 15817, Mar 2005.
Verifying Component Substitutability (ppt), Feb 2005.
Reachability Analysis for Asynchronous Systems (ppt), Nov 2004.
Symbolic Model Checking of Software (ppt), July 2003.

Courses/Teaching:

s07 - 15829 (Practical Decision Procedures)
s06 - TA:18341 (Logic Design Using Simulation, Synthesis and Verification Techniques)
f05 - 15853 (Algorithms in the Real World)
s05 - 17754 (Analysis of Software Aritifacts)
s04 - TA:18240 (Fundamentals of Digital Circuits), 15819 (Spec and Check)
f03 - 15814 (Type Systems)
s03 - 18841 (Dependability Analysis of Middleware Systems), 15820 (Model Checking+Theorem Proving)
f02- 18549 (Distributed Embedded Systems), 21600 (Math Logic I),
s02 - 15812 (Semantics of Prog. Languages), 21700 (Math Logic II)
f01 - 18751 (Applied Stochastic Processes), 18760 (VLSI CAD: Logic to Layout)

Personal:

I fight shy of making/observing any(all?) kind of descriptive utterances. I prefer metaphors, sign languages, keywords and completely vague references. Of course, my 'profession' hardly makes way for such a disposition, which further adds to my struggle.

keywords: music (hindustani, indian classical funk), poetry, lyrics, movies, dance, online social networks.

Links:

How/why not to get a PhD