Beyond Bug-Finding: Sound Program Analysis for Linux.

It is time for us to focus on sound analyses for our critical systems software--that is, we must focus on analyses that ensure the absence of defects of particular known types, rather than best-effort bug-finding tools. This paper presents three sample analyses for Linux that are aimed at eliminating bugs relating to type safety, deallocation, and blocking. These analyses rely on lightweight programmer annotations and run-time checks in order to make them practical and scalable. Sound analyses of this sort can check a wide variety of properties and will ultimately yield more reliable code than bug-finding alone.