5 ms·
I thought abstraction interpretation on the level that astree claims to implement is supposed to be extremely hard, which is why almost nobody else tries to do
by ryao 4y ago
I thought abstraction interpretation on the level that astree claims to implement is supposed to be extremely hard, which is why almost nobody else tries to do it. I only know of two that try:
http://kestreltechnology.com/technology.html http://kestreltechnology.com/technology.html
https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos
- edwcross 4y agoAlso Frama-C/Eva: https://www.frama-c.com/fc-plugins/eva.html https://www.frama-c.com/fc-plugins/eva.html
- mdaniel 4y agoIt took some eagle eye to spot the link, but they have the source in a self-hosted copy of gitlab: https://git.frama-c.com/pub/frama-c https://git.frama-c.com/pub/frama-c and a sibling repo is also interesting where they seem to apply analysis to some open source code as an example: https://git.frama-c.com/pub/open-source-case-studies https://git.frama-c.com/pub/open-source-case-studies
- mschnell 4y agoYou can add grammatech‘s codesonar
- marmetio 4y agoI believe the "level" referred to is soundness. Codesonar is self-admittedly not sound [1], and instead focuses on other valuable aspects of static analysis. It's a different type of tool. [1] https://blogs.grammatech.com/how-sound-static-analysis-complements-heuristic-analysis https://blogs.grammatech.com/how-sound-static-analysis-compl...
- quentinkent1 4y agoAlso Mathworks Polyspace Code Prover: https://mathworks.com/products/polyspace-code-prover.html https://mathworks.com/products/polyspace-code-prover.html
- sam_bristow 4y agoI _think_ Perforce's QA-C uses abstract interpretation, but I'm not 100% sure.