Welcome to my minimal web presence.
I am a member of Moshe Vardi's formal verification research group at Rice University.
My research focus is on the complementation and containment testing of Büchi automata, including: an experimental survey on complementation in CIAA'10 with M.-H. Tsai, Y.-K. Tsay, and M.Y. Vardi; a paper on subsumption in Ramsey-based universality checking in TACAS'10 with M.Y. Vardi (see also Abdulla et al.); and similarities between Büchi containment testing and Size-Change Termination, in TACAS'09 with M.Y. Vardi and in my Master's thesis.
I have the very helpful LaTeX symbols guide duplicated here. However, I highly recommend you check out the LaTeX Detexifier.
Many years ago, I worked with Seth Nielson and Dan Wallach on Google Desktop Security.
Information from an old set of OCaml tutorials can be found here .