Add a section on model-checkers / formal verification tools

[rurban]

Recommending just sanitizers or fuzzers is a bit too simplistic.
They might found vulns, but a model-checker will find all vulns, not on just the tested values which might appear in your test-suite.
Discuss benefits, limitations (loops and recursion).

Yes, I do use model checkers on my compilers and stdlib.

[kbeyls]

Thank you for making this suggestion, @rurban !
I agree that static analysis tools should also be covered, especially because they tend to be "compilers" of sorts themselves. I'm thinking of tools such as clang-static-analyzer. I wonder if you're thinking of a different class of tools when referring to "model-checkers"?

[kbeyls]

@all-contributors please add @rurban for ideas, bug reports

[allcontributors]

@kbeyls

I've put up a pull request to add @rurban! 🎉

[rurban]

Model checkers are formal verification tools, which cannot prove termination, but can symbolically verify functions. The best even within the C syntax, without any annotations.

cbmc is the industry standard, frama-c with it's plugins is also commonly used. The better ones are also used for crypto or kernels.