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.

• Type: Conference
• Year: 2007
• Where: HOTOS
• Authors: Zachary R. Anderson, Eric A. Brewer, Jeremy Condit, Robert Ennals, David Gay, Matthew Harren, George C. Necula, Feng Zhou
• Keywords: Analyses, HOTOS 2007, Operating System, Sample Analyses, Sound Analyses