Por Nuno Lopes (IST, ULisboa).

LLVM is one of the most widely used compilers in the world. Its users include Apple, Google, Meta, Microsoft, PlayStation, Qualcomm, and many others.

We started verifying LLVM a decade ago. In the process, we found bugs everywhere: in LLVM, in SMT solvers, in the documentation, and in our own tools. We also found shortcomings in the compiler’s theoretical models, namely of undefined behavior, memory, and concurrency. For example, we showed that it was impossible to run certain classic textbook optimizations together in LLVM. This led us to make fundamental architectural changes in LLVM itself.

Moreover, LLVM keeps changing every day. We caught many regressions along the way.

In this talk, we will cover our attempts to verify LLVM. The tools we built, the bugs we caught, the bugs we missed, the good and the bad surprises, and our contributions to theoretical models of compilers. We will also discuss why and how our automatic formal verification tools are used by compiler engineers on a daily basis.

Bio: Nuno P. Lopes is an associate professor at IST (U Lisbon). Previously, and has previously worked at Apple (US), Microsoft Research (UK and US), and Max Planck Institute (Germany). He is the inventor of 5 US and EU patents and has received 3 best paper awards from leading conferences, the HVC research impact award, and the HiPEAC tech transfer award.

Nuno has been an active open-source software contributor since 2003. His automatic compiler verification tool, Alive2, is used regularly by compiler developers around the world and has been officially adopted by the LLVM compiler.