Hacker News new | ask | show | jobs
by Nokinside 296 days ago
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

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

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...
1 comments
edwcross 295 days ago
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.
link