Should we balance? A preliminary study into the maintainability of formal specifications as Linux kernel source code evolves
Speaker (s):
Julia LAWALL
Senior Research Scientist
National Research Institute for
Digital Science and Technology
| Date: Time: Venue: | | 23 November 2026, Monday 3:30pm – 4:30pm School of Computing &
Information Systems 1 (SCIS 1)
Level 4, Meeting Room 4-4
Singapore Management University
80 Stamford Road
Singapore 178902 Please register by 22 November 2026 We look forward to seeing you at this research seminar. 
|
|
About the Talk
Today there is a renewed interest in formal verification of software, in part to thoroughly check that AI-generated code does what it was intended to do, and in part in recognition that critical code bases are becoming increasingly complex and a better understanding of their behavior is needed. Still, verifying a single code instance is not sufficient. It is also necessary to ensure that the code remains verifiable as it evolves. In this talk, we consider the latter problem in the context of a function used in the Linux kernel task scheduler. We find that simple changes in the code require only minor adjustments to the specifications and the verification process. More complex changes, however, can trigger situations that challenge the underlying SMT solvers used to make verification tractable. But we find that code inducing such challenging situations may also harbor bugs. The talk is based on the joint work with Keisuke Nishimura and Jean-Pierre Lozi presented at SAS 2024.
About the Speaker
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.
