Research Interests:
Software Verification, Programming Languages, Formal Methods, and Security (all with an emphasis on concurrency-related issues)
Projects:
- Recursive Program Synthesis: Synduce
- Reductions for Safety and Hypersafety Proofs: Weaver Verifier
- Parallel and Recursive 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
People:
Current Students:
- Ruotong Cheng (PhD)
- Danya Lette (PhD)
- Sky Li (MSc)
Former Students:
- Yi Zhao (MscAc, 2023)
- Victor Nicolet (PhD, Applied Scientist at AWS, Summer 2022)
- Zachary Kincaid (PhD, Associate 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)
- Aamod Kore(MSc 2019)
- Anthony Vandikas
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:
Constantin Enea, Andreas Podelski (U Freiburg), Philippa Gardner (Imperial College London)
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)