I forgot to add this one to my recent post about software defects:
"Why software fails", from the September 2005 issue of IEEE Spectrum. Take a look at their software hall of shame.
You can also read the last article in Simson Garfinkel's series in Wired. This one is "Microsoft's secret bug squasher" about using model checking and formal methods. For more about formal methods, see "The exterminators" in the September 2005 issue of IEEE Spectrum.