Open positions

I am looking for highly motivated postdocs interested in automata learning, reactive synthesis, algorithmic game theory and formal methods in general. If you are interested, please send me an email including your CV.


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 problems often lean on logic, automata theory, algorithmic game theory and machine learning.


Current Research

The current focus of my research is automata learning, in particular learning infinitary languages. Infinitary languages model reactive systems, and learning can be used for numerous problems related to design, verification and synthesis of reactive systems. If you are interested in this topic a good place to start is this survey paper or this invited talk.


My interest in learning formal languages followed my interest in 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. The following talk gives a short overview of PSL.


Editorial Boards

Logical Methods in Computer Science (2020 - present)

Program Committees

ICALP'23 (PC member), LICS'22 (Conf. Chair), RV'22 (PC member), MOVEP'22 (PC member), TACAS'22 (PC Co-Chair), LearnAut'22 (PC member), ICALP'21 (PC member), RV'21 (PC Co-Chair), CAV'20 (PC member), MFCS'19 (PC member), LearnAut'19 (PC member), CAV'19 (PC member), SYNT'19 (PC member), CAV'18 (PC member), SYNT'18 (PC member), SyGuS-COMP'14-18 (Co-Organizer), ICALP'17 (PC member), SYNT'17 (PC Co-Chair), SYNT'16 (PC member), SYNT'15 (PC member),


Steering Committees

LICS (2021 - present)
ETAPS (2020 - present)


Teaching

At the graduate level, I teach Automata and Logic over Infinite Objects as well as Infinite-Duration Games. At the undergradaute level, I teach Computational Models and taught once Principles of Programming Languages.



Fisman on the fly.



Fisman with loot.



Yet another Fisman.