Exploring the Journey of Academia to Industry and Back Again

Can you tell us a little bit about yourself, and about your research field?

Generally speaking, my research is about reasoning about infinite systems. The idea is that you have a system that has too many states, and you want to find out something about it—either to prove an interesting property, or find a violation of a security property, for instance.

I have been working for a long time in this field. Basically, I started working as a PhD in the area. After graduating my PhD I thought I don’t want to stay in academia, so I went to industry. I went to IBM—there was a small group in Haifa. I worked there with the compiling team, but then decided I wanted to go back to academia.

I went for a post-doc in Europe and the US, and came back to academia after that in 1998. I built a research group with fantastic students helping me. Many of them are now very well known. Returning to academia was definitely the right choice, I am very happy I took this decision.

About five years ago, my students and I decided it was the right time to bring our research into practice. This is how we began Certora, and it has been quite the undertaking—I’ve been putting in 24/7 work for this company. So, basically, I am back to my second love.

What services does Certora provide?

At Certora, we deal with billion dollar mistakes. We focus on mistakes in cryptocurrency software. For example, just a few weeks back, one of our clients lost 200,000,000 because they didn’t use our technology. In our approach, the challenging part is to extract the specification. But once we write it, we can prevent very expensive mistakes. Our technology is saving these people a lot of money, but it can be used for generic software as well.

Our clients are companies implementing some sort of arcade economic procedures on top of cryptocurrency. For example, you borrow money, but you borrow in cryptocurrency. Or you are doing some kind of exchange between different cryptocurrencies, or maybe there is some auction implemented in cryptocurrency.

What is interesting is that cryptocurrency is not backed by any physical asset. There is the concept of “makers” that use so-called stable coins, and some algorithms to trade on exchanges as a way to maintain a stable value on the market. At Certora, we were able to find a bug in one of these algorithms.

I have worked with companies like Airbus in the past, but the cryptocurrency software is more interesting as the code changes much more frequently, it is relatively small and modular. Therefore, there is much more potential for interesting analysis. Also, the properties of cryptocurrencies that are concise economic models are better understood.

Besides exploring the world of cryptocurrency, what other areas of research do you find most interesting and enjoyable?

Definitely, reasoning about infinite state systems, linked lists and data structures. I’m really interested in things like transitive closures, reasoning about infinite state systems where you actually have the ability to say something that is not expressible even in first order logic, but you can still reason about. Throughout my career, I have been concerned with identifying and reasoning about interesting properties of tiny programs. Many other people look into more scalable things.

An interesting result I achieved was to show that, for example, effectively propositional logic (EPR), which is a weak form of first order logic, can be used to reason about many, many of the things monadic second order logic was used for. The idea was to exploit a very weak logic to reason about many things. This is something that I’ve been fortunate to work with many outstanding students. It took us a little bit initially to convince the community that was wondering why we were using such weak logic after showing them how to use powerful logic. So the EPR result was very interesting. I’m also very acknowledged today.

When I transitioned from academia to industry, I learned a lot in the corporate world before returning to academia. Furthermore, I worked very closely with Thomas Reps and Susan Horwitz, and they were really instrumental to my career. We came up with this idea about interprocedural analysis. So this is now the standard. We actually worked on this together day and night and came up with the basic algorithms published in POPL’95. This was integrated into SLAM, device driver and into Facebook. We relied on the seminal work of Sharir and Pnueli that preceded us, but it was not well understood. We actually made it easier to understand and use it. Thomas also continued to work on it. So, I think this is the second contribution, which was very, very interesting for me.

However, what I really like about my career is working with people. I’m a people’s person. I work with many, many people and many, many people work with me. I’m a communicative person.

Can you tell us something about the most exciting current technical advances in your field?

I see a lot of potential in many, many things. I see that the field is kind of moving in two complementary directions. Some work is concerned with high-level views of things. For instance, the work of Thomas Henzinger and others focuses on far-reaching ideas such as quantum computing, and related aspects. And another line of work, which is equally important and closer to Certora, is concerned with making the technology that other people have developed before us in the 70s or the 80s more available for industrial standards.

As an employee of Certora, my primary concern is the second direction. At Certora, we are more interested in the engineering side, and in understanding how to exploit technologies such as SMT solvers, Z3 or cvc5, for instance, for solving real-world problems. However, as an academic, I am more focused on the first direction, as it deals with more far-reaching ideas. I’m trying to understand: How to reason about systems? What is the right model for those systems?

If you could give your younger self advice, what would it be?

Very interesting question. So, basically “what mistakes I have made” is what you’re asking? I have made many mistakes. I guess focusing and consistency are not my strengths. I think of too many things.

This was not the case for my shape-analysis work that we very much focused on, despite everybody saying it was a bad topic. I remember giving a talk and everybody saying it’s not interesting, but I loved the work. I think for academics it’s really, really hard sometimes. Academia really sees fashions. So, I wish myself and others: look at the fashion, but once you are up to something, focus on it. I think this is something that I’ve already done, and I could have done it even a bit better.

What is your approach to attracting students into more fundamental research that is maybe not fashionable at the moment?

Sometimes it was very difficult for me to attract students. One approach was to take students when they were very young. I tried to attract them when they were even in their undergrad. The second approach, somehow different from what many of my colleagues have done, was to focus on having three or four very good students and spending enough time with them. This is how I got more results than some people having maybe ten students. Later on, when my group got larger, I probably had more impact, but it became more difficult to give everyone the individual attention they needed. It depends, of course, but I think staying small it’s a good idea.

Also, there is some advantage of working in a smaller field because you can celebrate it. You can celebrate the fact that you understand everything. If students come to you and say they want to do something fashionable, tell them to do it. You will find a way to attract the ones that you want, even if these are fewer people. People are people, and if they see some interesting things, they might hope they will get it.

Which expert would you like to have featured on the ETAPS blog?

Many, many people are doing a lot of cool things. Also, young people are doing very, very good things. Just to name a few: Ori Lahav (TAU), Derek Dreyer (MPI), Rupak Mujumdar (MPI), Tom Henziger (IST), Martin Vechev (ETH Zurich), Laura Kovacs (TU Vien) and Alexandra Silva (Cornell). It would be nice to see people like me transitioning from academia to industry, as well as those making the reverse journey.