Commenter Jeff asks what the PRE in PREfast stands for.
It's an inside joke.
The Microsoft Programmer Productivity Research Center (MSPPRC) originally produced a tool called PREfix. Michael Howard put me in touch with the development team, and they explained that it was called PREfix because it helps you fix your bugs before (PRE) you even run the code.
The problem with PREfix was that it required monster hardware, and even if you got the hardware up and running, the results took days to generate, and tuning the program's parameters required intricate knowledge of its inner workings. In other words, it was something only a researcher would love.
When they started sharing the tool with the product groups, the response was as you might expect: "This is great stuff you guys have here, but it's kind of impractical to expect everybody to have hundreds of thousands of dollars of hardware and a Ph.D. in order to run it."
The solution was a lightweight version of PREfix, which was named PREfast because it was a fast version of PREfix. It didn't do as thorough a job, but it didn't require monster hardware and could be understood by people who didn't have a brain the size of a planet.
In a sense, Jeff asked the wrong question. The real issue is not what the PRE stands for; it's what the fast stands for!