5 ms·
>I don't think you can. Having done it, I'm pretty sure you can. Why don't you think it can be done? It requires a programming language (or language subset) w
by NovemberWhiskey 3y ago
>I don't think you can.
Having done it, I'm pretty sure you can. Why don't you think it can be done?
It requires a programming language (or language subset) with very well-defined semantics, and the use of theorem-proving tools but it's certainly possible.
- AnimalMuppet 3y agoYou'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.