I am a research scientist at UPenn, working in the area of formal verification. In the past I touched topics in the area of model checking, temporal logic, parameterized systems and reactive synthesis.

One focal point of my work was the laying of a firm mathematical foundation for industrial-oriented temporal logics. These works had a major impact on the IEEE standards PSL (IEEE-1850) and SVA (IEEE-1800). The chapter Cindy Eisner and I wrote for the handbook of model checking summarizes these works.

Recently, I became interested in algorithmic game theory and computational learning theory and I am trying to utilize ideas from these areas to the area of formal verification. See the Rational Synthesis paper with Orna Kupferman and Yoad Lustig, and the Learning Regular Omega Languages paper with Dana Angluin.