It is the year 2025. FutureCorp, the private
sector defence contractor to whom the US government has
outsourced its management of nuclear weapons, has just
had its missile control software hijacked by terrorists. It
is only a matter of hours before Armageddon. The CEO
of FutureCorp, Dr F. Methods, is incredulous: “This is
impossible”, he told one of our reporters. “We used program
analysis to formally prove that the software was secure!”.
“Ah, Dr Methods,” responded open-source developer Mr B.
Door, “But did you check the analyser?”