My research area is broadly referred to as formal methods in system design. The research questions are derived by the need to increase the reliability of computerized systems (or programs) and the assurance of their correctness. The metods for solving these problem often lean on logic, automata theory, algorithmic game theory and machine learning.

Current Research

The current focus of my research is program synthesis. The traditional formulation of program synthesis is to transform a declerative specification of what the system should do to an implementation of the system. Today we view program synthesis in a more relaxed form and consider a specification scale where on one end of the scale we have a complete rigorous mathematical specification (e.g. a set of temproal logic formulas), somewhere in the middle we have partial specifications and/or partial implementations and on the other end of the scale we have only examples.

Here are some of my publicatios along this scale, left to right:
Learning Regular Omega Languages with Dana Angluin
Syntax-Guided Synthesis with Rajeev Alur and many others
Rational Synthesis with Orna Kupferman and Yoad Lustig.
For more publication see here.

Past Research

One focal point of my work was the laying of a firm mathematical foundation for 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. We also authored a book on PSL, aimed for users of the language.

Recent Community Service

ICALP'17 (PC), SYNT'17 (co-chair), SyGuS-COMP'16 (co-organizer), SYNT'16 (PC), SyGuS-COMP'15 (co-organizer), SYNT'15 (PC), SyGuS-COMP'14 (co-organizer)


Spring 2017: Principles of Programming Languages

Fall 2016: Automata on Infinite Words

Fisman on the fly.

Fisman with a loot.

Yet another Fisman.