5 ms·
Is C++ complex enough that it is difficult to model, and therefore hard to apply in formal methods?
by pensono 6y ago
Is C++ complex enough that it is difficult to model, and therefore hard to apply in formal methods?
- rurban 6y agoThe problem is not the language, the problem are unbounded loops. Like linked lists vs vectors. Termination is theoretically impossible to prove, but practically you can handle it. Parts of the STL were formally verified. cprover (with satabs and cbmc) can handle C, C++ or Java. F' uses autogenerated classes, which helps a lot avoiding mistakes.
- gugagore 6y agoBecause the problem is unsolvable, there is a wide variety of "you can handle it"-ness that a language can have...