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. Take a look at my research page, and send me an email if any of the topics interest you. Feel free to come forward with your own ideas as well.

Current Collaborators:
Constantin Enea (University of Paris 7), Andreas Podelski (U Freiburg)

Former Collaborators:
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)