[b-man]

> While such techniques are available, would they be really applicable in a very dynamic environment such as with millions of PCs running various windows versions, needing continuous / real-time updates.

I don't see much difference in complexity between the affected software and the several existing formally verified software. At the very least the parser/interpreter could very much be formally verified.

But my point is, have they tried? They don't seem to be even aware of such.