The bleeding edge uses abstract interpretation to verify code.
Free from NASA:
IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation. https://github.com/NASA-SW-VnV/ikos
On the free side, you also have Frama-C (https://www.frama-c.com) and its Eva plug-in, based on abstract interpretation, and Mopsa (https://mopsa.lip6.fr), also based on abstract interpretation.
The bleeding edge uses abstract interpretation to verify code.
Free from NASA: IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation. https://github.com/NASA-SW-VnV/ikos
Commercial: Astrée is a static analyzer for safety-critical software written or generated in C or C++. https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm
abstract interpretation for static analysis and verification:
Good intro Mechanized semantics, fifth lecture Abstract art: static analysis by abstract interpretation https://xavierleroy.org/CdF/2019-2020/5.pdf
Static Analysis and Verification of Aerospace Software by Abstract Interpretation https://mine.perso.lip6.fr/publi/article-bertrane-al-fntpl15...