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/REA... 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 if you have money.