These tools are essential for any driver writer and the folks who work on them are just down the hall from me.  PFD is your normal PreFast with additional rules about kernel functions.  SDV (static driver verifier) is a completely different tool which simulates a kernel environment and tries to find bugs in that simulation.

You can read the article here.