Subodh Sharma

Subodh Sharma

Associate Professor and Pankaj Gupta Chair Professor in Privacy and Decentralisation



My research is primarily in the area of software engineering and formal methods. I am interested in ensuring the reliability of parallel software via static and dynamic program analyses, model checking, and PL solutions. I am also interested in employing HPC towards the creation of scalable verification technology. My recent research investigations have been in the area of systems security, data privacy, and Blockchain.

Prior to joining the Department of Computer Science and Engineering at IIT Delhi, I worked as a post-doctoral researcher in the Systems Verification group at the University of Oxford.

I am associated with the VerTeCS research group@IITD and also an associated faculty member in the School for Public Policy.

  • Formal Verification
  • Program Analysis
  • Systems Security, Data Privacy
  • High Performance Computing
  • PhD in Computer Science

    University of Utah


Note for prospective students (MS/PhD/Interns)

I am looking for motivated students who are good in mathematics and programming and are interested in pursuing research (MSR/PhD) in the broad areas of verification, program synthesis, and security. If you are interested, drop me an email with your resume with the subject tag [ResearchApplicant]. Note that the admission in to the program will be through the regular admission process for MSR/PhD students (refer the cse@iitd admissions page for details). For internships, the expected time commitment from students is at least six months.

Recent Publications

Quickly discover relevant content by filtering publications.
(2021). Synthesizing Multi-threaded Tests from Sequential Traces to Detect Communication Deadlocks. In ICST 2021.

(2020). Security Types for Synchronous Data Flow Systems.. Accepted in MEMOCODE 2020.

(2020). Verifying and Testing Concurrent Programs using Constraint Solver based Approaches. In ICSME 2020.

PDF Cite

(2020). Privacy concerns with Aadhaar. In ACM CACM 2019.

PDF Cite

(2018). Dynamic Symbolic Verification of MPI Programs. In FM'18.

PDF Cite




  • Deepak Kunwar
    MTech Thesis: Automatic Verification of Sequential Consistent Memory Concurrency

  • Namrata Jain
    MTech Thesis: Verification and Synthesis of Smart Contracts
    First employment: Microsoft

  • Arpit Aggarwal
    MTech Thesis: Bounded Model Checking of Go Concurrency
    First employment: Oracle

  • Deepanker Mishra
    MTech Thesis: Parameterized Verification of Message Passing Programs
    First employment: Nutanix

  • Garvit Jain
    MTech Thesis: Parameterized Verification of Message Passing Programs

  • Abhishek Khuntwal
    MTech Thesis: Efficient Parallelization of DPOR
    First employment: Nutanix

  • Ronak Khandelwal
    MTech Thesis: Runtime Verification of C11 Concurrency
    First employment: Worldquant

  • Guarav Gupta
    MTech Thesis: Accelarating SSL Computations Via GPUs
    First employment: Adobe