Spotlight: Aws Albarghouthi

Our “New Scientists on the Block” series features up-and-coming PL researchers who are about to begin independent research careers in universities or research laboratories. This week, we  interview Aws Albarghouthi, who is starting as an assistant professor at the University of Wisconsin, Madison, in January 2015.

Tell us a bit about your academic background.

I am currently finishing up my PhD at the University of Toronto. In January, I will be joining the University of Wisconsin-Madison as an assistant professor in the Computer Sciences Department. Before all of this, I was an undergraduate student in the software engineering program at McMaster University in Hamilton, Ontario (about an hour south-west of Toronto). At McMaster, there was a huge (almost religious) emphasis on formal methods for software design. Long story short, I contracted the disease, and this led me to research heavy-weight software verification and program analysis techniques in graduate school. Over the past few years in graduate school, I spent three delightful internships at Microsoft Research in three different labs in three different continents: Bangalore (India), Redmond (US), and Cambridge (UK). To the best of my knowledge, I am the first to complete the coveted MSR hat-trick!

What is the sort of research that you like to do?

At a high level, I like to work on problems of practical interest that are intellectually stimulating (from a mathematical and logical perspective). Most of my research has been on different aspects of automated software verification: proving that a program, for instance, has no runtime errors. This classical problem is obviously of practical interest (wouldn’t it be nice to make sure programs don’t crash?) and has been a major subject of study in the PL community. For my PhD, I primarily worked on logic-based techniques for automatically verifying software. Specifically, I introduced new efficient interpolation-based verification techniques. What does that mean? Simply speaking, Craig interpolants are artifacts of first-order logic that can be used (as Ken McMillan showed us) to generalize a proof of a finite number of cases to a proof of many cases. So, when talking about programs, we can examine a small fragment of the program, and use interpolants to hypothesize a proof of the whole program! My work on the area resulted an award-winning C verification tool, called UFO (check it out!), that implements some of my verification algorithms.

We’d like to read one paper of yours to get a flavor of your work. Which one should that be, and what’s it about?

I would suggest reading “Beautiful Interpolants”, a CAV 2013 paper that I wrote with Ken McMillan. The abstract intuition is that a simple, elegant explanation of a phenomenon is more likely to be correct than a complex one (Occam’s razor, if you will). We apply this idea to constructing proofs of programs. When using an interpolant to generalize a proof of a program fragment to the whole program, we look for a simple (beautiful) interpolant, with the hope that a beautiful interpolant is more likely to capture the essence of a proof of correctness. I chose this paper because it’s easy to read and because I believe it neatly conveys the intuition behind interpolation-based verification.

What new problems are you exploring, or plan to explore once you start your faculty job?

First, despite the amazing advances in automated verification, there remains a huge number of open problems (and they seem to be monotonically increasing). So I would like to keep pushing in this direction, for instance, by extending my techniques to concurrent program verification and precise handling of heap data structures. Second, I believe the PL and verification research communities have a lot to offer to other disciplines, and we are starting to witness some very promising interactions, for example, in software-defined networking, MOOCs, and security. So I would like to explore new problems where automated verification and synthesis can be beneficial. For instance, I plan on applying synthesis and verification techniques for aiding in the design and implementation of eventually-consistent data structures, where a lot of non-trivial interactions have to be dealt with between different replicas of the same data structure. This is a problem of increasing importance in our modern distributed world.

What are the things about PL research and the PL community that you like the most?

I like how the community and the field are uniquely positioned between theory and practice. There are lots of interesting theoretical questions to be asked when designing programming languages and program analyses. Simultaneously, our techniques and tools can (we hope) transform how software is written, read, compiled, and executed.

What would you like to see more of in the PL community?

I was very happy to see the announcement for this blog, and I’ve been following your great posts! I am envious of other research communities, particularly the theory community, for having a good number of high-quality blogs by top academics. So, I would like to see more initiatives like The PL Enthusiast. On another note, I would like to see open access for conference proceedings. The papers of most top systems conferences, for instance, are freely available online (with videos of the talks), and I do not really see why we cannot do the same for our conferences.

What advice would you have for graduate students who want a faculty job in the next couple of years?

In terms of being on the job market and applying, it is a long and opaque process. I found talking to a lot of people, particularly those who had recently been on the job market, to be very helpful. So, seek advice and criticism (e.g., on your application materials and talk) from mentors and peers. Also, make sure schools you apply to know about your application. If you don’t personally know people at some school, ask your advisor, mentors, or co-authors to send an email on your behalf — it is amazing how much people are willing to help!

A lot has been written on how to apply, interview, etc. I found these two resources to be the most informative:

(1) Computer Science Grad Student Job Application & Interview Guide, by Westley Weimer and Claire Le Goues

(2) How to get a faculty job, by Matt Welsh (4 blog posts; the link goes to the first one).

I liked (1) for its level of detail, which makes you know what to expect from the process. For example, it provides exact timelines of when the two authors received their interview invitations, when they had their interviews, and when they got their offers. The blog posts of (2) have many debates between professors in the comments (it turns out academics have strong opinions on what candidates should (not) wear to an interview).