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 methods 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 declarative 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 temporal 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
Search-based program synthesis with Rajeev Alur, Rishabh Singh and Armando Solar-Lezama
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.

Program Committees

MFCS'19 (PC), LearnAut'19 (PC), CAV'19 (PC), SYNT'19 (PC), CAV'18 (PC), SYNT'18 (PC), SyGuS-COMP'18 (co-organizer), ICALP'17 (PC), SyGuS-COMP'17 (co-organizer), 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)


For graduatem I teach Automata and Logic over Infinite Objects or variations thereof. For undergradautes, I teach Automata, Formal Languages & Computability and taught once Principles of Programming Languages.

Fisman on the fly.

Fisman with loot.

Yet another Fisman.