This Linux kernel is a long-lived, large, and widely used piece of software. It was first released in 1994, currently amounts to over 27 MLOC, and is used everywhere, from smartphones to supercomputers. Despite its more than 30 year history, the Linux kernel is still under active development, being continually extended with new features, but also new designs, to improve performance, understandability, safety, and security. In 2004, my colleagues and I started to work on Coccinelle, a tool for automating the large-scale transformation of C code, designed with the needs of Linux kernel developers in mind. Today, Coccinelle is a familiar element of the kernel developer’s toolbox, having been used in thousands of kernel commits. However, not all software issues can be neatly characterized as collections of common code patterns. We thus propose to complement Coccinelle as a kernel development tool with strategies for tracing kernel execution and formal verification.

Julia Lawall received the Ph.D. degree in 1994 from the Indiana University. She has been a senior research scientist at Inria since 2011 and head of the Whisper team since 2021. Previously, she was an Associate Professor at the University of Copenhagen. Her research interests are in the area of improving the quality of infrastructure software, using a variety of approaches including program analysis, program transformation, and software verification. She develops the tool Coccinelle that is extensively used in the development of the Linux kernel and she has over 2000 patches in the Linux kernel based on this work.