That's just start. The bleeding edge uses abstract interpretation to verify code. Free from NASA: IKOS (Inference Kernel for Open Static Analyzers) is a stat

That's just start. 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 https://github.com/NASA-SW-VnV/ikos Commercial: Astrée is a static analyzer for safety-critical software written or gen­er­ated in C or C++. https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm 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 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.pdf https://mine.perso.lip6.fr/publi/article-bertrane-al-fntpl15...