Speaker
Julia Lawall
(Inria)
Description
Program verification, ie, producing a proof that code matches its specification, can be seen as the ultimate form of bug finding. Nevertheless, program verification is widely considered to be difficult and time consuming. Furthermore, in the case of the Linux kernel, any verification effort is likely quickly out of date, given the rate of change in the code base. Still, it is not necessarily the case that a change in the source code will have an impact on the specifications or their proof. In this talk, we present our experiments on applying verification to the Linux kernel scheduler, studying the resistance to change of the verification effort and the bugs and missed optimization opportunities found.
Primary author
Julia Lawall
(Inria)
Co-authors
Jean-Pierre Lozi
(Inria)
Keisuke Nishimura
(Inria)