2 ms·
In addition to other good answers, there is also the fact that verification doesn't necessarily have to be "deep": "shallow" verification of only some security
by tom_mellior 9y ago
In addition to other good answers, there is also the fact that verification doesn't necessarily have to be "deep": "shallow" verification of only some security properties can also be very useful. For example, it may be hard to verify the "correctness" of a web server since the specification of what a web server should do is quite complex.
But (for example, for a web server written in Ada or C) you can also do without a specification and just apply verification tools to only check things like "all memory accesses are valid", proving that you have no buffer overflows that would cause denial of service or security holes.
Of course someone still has to write the verification tool correctly to ensure that it actually gives the safety guarantees you want, but at least it's not you who has to worry about that ;-) And specifying the absence of buffer overflows is comparatively simple.