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

  • Reductions for Safety and Hypersafety Proofs: Weaver Verifier
  • 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:
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)