4 ms·
Not an expert, but: Currently formal verification is complicated, expensive, and can only be used for verifying small amounts of code. And if you look at the p
by hershel 13y ago
Not an expert, but:
Currently formal verification is complicated, expensive, and can only be used for verifying small amounts of code. And if you look at the places where it's highly valuable , i.e. security,hardware design and critical/medical systems - i don't see a wide deployment there. So not good signs.
And i heard of formal verification tools for c#, ada, and c/c++.
- munin 13y agoI have been told that this is only the case in America (and I guess Asia). in Europe, there are laws that require the use of safety-validation tools and worst-case execution time tools on code that will be used in safety critical applications, for example, flight control, process control, etc.
- hershel 13y agoSafety verification tools - like static analysis/timing analysis - is different from full formal verification. Those tool run on their own and don't need complex definition of what to verify , and they verify just small amount of bugs.
- cantankerous 13y agoLook at aerospace and aeronautics. It's becoming par for the course there.
- sliverstorm 13y agoI don't know if formal code verification is much like hardware verification, but modern hardware like microprocessors and larger FPGA designs undergo verification... and it is so impossibly computationally expensive, the key exercise becomes selecting the most important 0.1% of coverage. So, if they are similar pursuits, I can't help but imagine complete formal verification of large modern codebases would also be essentially computationally impossible.