Software verification tools based on abstract Interpretation are really good today. If you want free software I recommend IKOS - a is a sound static analyzer

Software verification tools based on abstract Interpretation are really good today. If you want free software I recommend IKOS - a is a sound static analyzer for C/C++ developed at NASA. Checks: https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/README.md#checks https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA... Numerical abstract domains: https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/README.md#numerical-abstract-domains https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA... Commercial tool like Astree https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm if you have money.