Most of my research is in automata-theoretic formal verification, dealing with complementation, determinization, and containment checking for Büchi automata.
- Random Models for Evaluating Efficient Büchi Universality Checking (with C. Fisher, M.Y. Vardi in ICLA'17)
- Subsumption Trees for On-The-Fly Universality Checking of Finite-State Automata (with E. LeGros in YR-ICALP'15, abstract)
- Profile Trees for Büchi Word Automata, with Application to Determinization (with O. Kupferman, M. Y. Vardi, Th. Wilke. in I&C'15, extended verison of GandALF'13)
- Unifying Büchi Complementation Constructions (with O. Kupferman, M. Y. Vardi, Th. Wilke. in LMCS'13 , extended version of CSL'11)
- State of Büchi Complementation (with M.-H. Tsai, M.Y. Vardi and Y.-K. Tsay in LMCS'14, extended version of CIAA'10).
- Efficient Büchi Universality Checking (with M.Y. Vardi in TACAS'10 )
- Büchi Complementation and Size-Change Termination (with M. Y Vardi in LMC'12, full version of TACAS'09).
I also work with programming languages, most recently in domain-specific languages.
I briefly dabbled in security in graduate school, and maintain an interest.