##
Overview

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

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.

##
Program Committees

CAV'18 (PC),
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)

##
Teaching

Spring 2018: Automata and Logic on Infinite Objects

Fall 2017: Automata, Formal Languages & Computability

Spring 2017:
Principles of Programming Languages

Fall 2016:
Automata on Infinite Words