Rohit Sinha

GitHub rsinha

Codeplex rsinha



Research Interests

I work on applying mathematical proof techniques to reason about software security. My research focuses on proving that a security-critical program demonstrates end-to-end security by modeling programs in a formal system (e.g. first-order logic) and using formal analysis (e.g. theorem proving, type checking) to prove an absence of errors. Specifically, I am using these techniques to build provably correct security-critical applications to run on trusted hardware such as Intel SGX. I am being advised by Prof. Sanjit Seshia at UC Berkeley, where I am currently pursuing my PhD in Electrical Engineering and Computer Science.


  1. A Design and Verification Methodology for Secure Isolated Regions (PLDI 2016)

  2. Moat: Verifying Confidentiality Properties of Enclave Programs (CCS 2015)

  3. Automatic Rootcausing for Program Equivalence Failures (CAV 2015)

  4. Formal Modeling and Verification of CloudProxy (VSTTE 2014)

  5. Symbolic Software Model Validation (MEMOCODE 2013)

  6. Verification with Small and Short Worlds (FMCAD 2012)

My undergraduate research in design automation resulted in the following publications:

  1. Parallel Simulation of Mixed-abstraction SystemC Models on GPUs and Multicore CPUs (ASPDAC 2012)

  2. Abstract State Machines as an Intermediate Representation for High-level Synthesis (DATE 2011)