4 ms·
You've done it? For how big a program? And, for how many aspects? You can determine the absence of type problems; you can determine the absence of buffer ove
by AnimalMuppet 3y ago
You've done it? For how big a program?
And, for how many aspects? You can determine the absence of type problems; you can determine the absence of buffer overruns and use-after-free. Can you determine the absence of race conditions? Can you determine that it meets timing constraints with 100% certainty?
There are a huge number of different kinds of things that a specification could specify. I'm pretty sure that we can't formally verify all of them.
- NovemberWhiskey 3y agoProof of absence of run-time exceptions and proof of correctness for a part of the system. This was for the air-data computer of a fighter aircraft. The programming language used had no dynamic allocation, so no use-after-free; and it was single-threaded so no race conditions. We did prove that there were no array indexing errors (i.e. buffer overruns). Recursion is also not permitted, so maximum call-stack depth is determined as well.