Please visit my new homepage at https://www.cs.bgu.ac.il/~dana/


Research Interest

I am a research scientist at UPenn, working in the area of formal verification. Some of the topics I worked on include model checking, temporal logic, parameterized systems, reactive synthesis, program verification and program synthesis.


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.


Recently, I became interested in algorithmic game theory and computational learning theory and my current research is a coallescence of these areas and the area of formal metods. See the Rational Synthesis paper with Orna Kupferman and Yoad Lustig, and the Learning Regular Omega Languages paper with Dana Angluin.


Current Activities

I am the associated director of the NSF Expeditions in Computer Augmented Program Engineering ExCAPE, led by Rajeev Alur. ExCAPE's aim is to develop synthesis tools that can assist expert programmers to discover tricky parts of the code, and/or help end-users perform simple programming tasks without having to write code.


I am a co-organizer of SyGuS-COMP'16, the third competition of solvers for Syntax-Guided Synthesis (SyGuS). SyGuS is the problem of synthesizing program fragments from a given description of both logical and syntactic constraints.


Recent Service

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





Fisman on the fly.



Fisman with a loot.



Yet another Fisman.