C Tooling
tomscheers.github.io
tomscheers.github.io
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...