by Georgiana Caltais — 19 September 2023
Can you tell us a little about yourself, and about your research field?
I am a faculty member at the School of Computer Science and Engineering at The Hebrew University. My research focuses on the theoretical aspects of formal verification. I study automata theory, logic, game theory, and their applications in verification and synthesis of reactive systems. It is easy (at least for readers of the ETAPS blog) to recognize the connection of automata and logic to verification and design—we employ automata and logic to specify desired behaviors. Let me elaborate a bit about the connection of game theory: a reactive system interacts with its environment. During the interaction, the system and the environment together generate a computation; for example, by repeatedly assigning values to input and output signals. A correct system must satisfy its specification in all environments, and can thus be viewed as a winning strategy in a game in which the players, namely the system and the environment, interact and generate a computation. The system wins if the generated computation is correct. In this perspective, the synthesis of a correct system reduces to finding winning strategies in games.
What have been the most rewarding aspects of your career in computer science?
The first things that come to mind transcend the specific discipline of Computer Science and relate to the general joys of being a researcher, particularly in academia. I have the freedom to choose the direction of my research and the problems I wish to explore. Research is complemented by mentoring students, writing and undergraduate teaching, all of which I cherish. I am privileged to be part of a vibrant international community, allowing me to meet many wonderful colleagues with diverse backgrounds. Over the years, I’ve gained a long-term perspective on how research evolves within a field, which I find fascinating. On top of all this, I find my research area very interesting and challenging. My work is my hobby.
What projects have you been most proud of throughout your career?
Well, it’s not really a project, but I am very happy about the decision to focus on contributions that are in the theoretical side of formal methods. I believe it’s regrettable that many PhD theses concentrate on implementations rather than exploring improved theoretical foundations, new concepts, interdisciplinary ideas, and fresh perspectives. Certainly, pure theoretical research should remain mindful of applications, and experimental results do provide insights into the feasibility of new ideas. Nevertheless, I believe that our responsibility (and privilege) in academia is to develop the theoretical foundations and nurture the next generation of researchers. The development of tools is undoubtedly valuable, but it requires and emphasizes skills that should be secondary in PhD studies, in particular that it involves a lot of overhead. I think it should be left to the industry.
What is your favorite success story that you’ve seen as a result of your work as a computer scientist?
These are very unusual times in Israel. Our government is pushing through legislation that is undermining judicial independence and fundamentally undermining Israel’s democracy. This is an imminent threat to Israeli academia, which relies on a solid democratic foundation, freedom and equality. I am extremely proud of the very active role that the High Tech industry in Israel is taking in our protest against the government. In one of the demonstrations in Tel Aviv, protesters wrote a huge P=NP graffiti on the highway. When I saw it, I felt we did something very good in the education we give our students. I think that computer scientists are in a position to have a lot of influence in shaping the future, and it’s crucial that the curriculum and the whole learning experience include elements that would direct our students to do good things with the power they have.
On the research front, it is very nice to see how alternating temporal logic, which I developed in my postdoc with Rajeev Alur and Thomas Henzinger, has found utility in AI, an application we did not initially have in mind when developing it.
What do you think will be the most exciting advances in computer science in the next five years?
Rather than responding, I will paste the prefix of my conversation with ChatGPT now:
Orna: I am responding to a set of interview questions for a computer-science blog. I would greatly appreciate your insights on the following query: “What do you think will be the most exciting advances in computer science in the next five years?”
ChatGPT: Predicting the future of computer science is always a bit speculative, but I can certainly provide some insights into areas that have been showing promising developments and are likely to be exciting in the next five years: …
This came with a list of ten interesting areas, which you can generate yourself. Anyway, they include nothing about our area, so I wanted to teach ChatGPT to have some more respect to formal methods:
Orna: Do you think that we will also see interesting advances in the field of formal verification and synthesis?
ChatGPT: Yes, it’s highly likely that we will continue to see significant advances in the fields of formal verification and synthesis in the coming years. These areas are crucial in ensuring the correctness and reliability of complex software and hardware systems, and they play a vital role in various domains, including safety-critical systems, autonomous vehicles, aerospace, and more. Here are a few reasons why we can expect interesting developments: …
This came with ten interesting reasons, which you can generate yourself.
What do you believe are the most successful strategies for promoting DEI in the field of computer science?
It is evident (and supported by substantial research) that, in terms of abilities, there is no group that is inherently superior for success in computer science. Nonetheless, we have yet to achieve full diversity, equity and inclusion (DEI) in CS. I believe the reasons for this issue lie in the years before and after students’ time at the university. Before university, children are exposed to social constructs, especially stereotypes suggesting that women do not belong in STEM fields. After university, High Tech careers are often portrayed as challenging to balance with parenting. Since I have never worked in the industry, it is challenging for me to comment on the latter issue. Regarding the former, I am not a proponent of strategies that attempt to make CS more inviting by, for example, introducing pair programming or emphasizing interdisciplinary combinations of CS with other fields like biology or cognition. While these practices may indeed benefit CS regardless of their DEI aspects, I disagree with the underlying DEI notion that “CS needs to be made more engaging or connected to real-world applications to attract women.” Instead, I believe we should strive to challenge and dispel stereotypes.