Research Interests:
Software Verification, Programming Languages, Formal Methods, and Security (all with an emphasis on concurrency-related issues)

  • Parallel Program Synthesis: Parsynt
  • Concurrent Program Proofs based on Data Flow
  • Parameterized Concurrent Program Verification: Duet
  • Concurrent Program Testing: Penelope
  • Con2colic Testing: concurrent program test generation with ConCrest
  • Consistency Verification of Decision Making Programs under Numerical Uncertainty
  • Verification of Finite-Precision (floating point) Programs


Current Students:
Former Students:
  • Zachary Kincaid (Assistant Professor in Princeton, Fall 2016)
  • Nilloofar Razavi (PhD, Fall 2013)
  • Matthew Amy (Fall 2013-2015)
  • Golnaz Ghasemi: (MSc, Winter 2011)
  • Jonathan Eidelman (Msc, Spring 2017)
I am always looking for highly motivated students who would like to work in my research area. Send me an email if any of the topics interest you. Feel free to come forward with your own ideas as well.

Current Collaborators:
Philippa Gardner (Imperial College London)

Former Collaborators:
Constantin Enea (University of Paris 7), Andreas Podelski (U Freiburg), Swarat Chaudhuri (Rice), Edmund Clarke (CMU), Helmut Veith (TU Vienna), Yu-Fang Chen (Academia Sinica), Sheila McIlraith (U Toronto), Madhusudan Parthasarathy (UIUC), Bow-Yaw Wang (Academia Sinica), Yih-Kuen Tsay (NTU)