Home

My research interests are broadly in the area of investigating reasons, causes, and explanations of software engineering and machine learning procedures. Historically, I first investigated the reasons and causes for the results of verification of hardware and software systems. Formal verification amounts to automatically proving that a mathematical model of the system satisfies the formal specification. Problems arise when answers are not accompanied by explanations, thus reducing users’ trust in the positive answer and the ability to debug the system in case of errors. I brought the concepts of causality from AI to formal verification and demonstrated their usefulness to the causal analysis and explanations of verification procedures. Together with Joe Halpern, I wrote a paper that introduces quantification to the concept of causality, thus allowing to rank the potential causes from the most influential to the least influential and to focus on the most influential causes. I pioneered the use of the concepts of causality in software engineering, resulting in first industrial applications (explanations of counterexamples produced by an IBM hardware verification tool and efficient evaluation of hardware circuits in Intel).

My current research focus in the area of causes and explanations is mostly on the explanations of the results of deep neural networks’ decisions. I also have an ongoing research project on explanations of reinforcement learning policies.

In other directions, I have an ongoing research activity in the area of hardware synthesis, collaborating with Tu Graz and the Technion, and in the area of learning for software analysis and exploration, collaborating with Ben-Gurion University.