Software will always have bugs, but some bugs are preventable. For example, both Heartbleed and the recent Apple SSL bug could have been detected with static analysis. I developed the Smatch static analysis tool to prevent these sorts of bugs in the Linux kernel. It has been very useful and resulted in around two thousand patches.
This talk is an introduction to Smatch with some of the theory, a description of what Smatch is able to do right now, and what some of the goals are.