Astrée Static Analyzer for C and C++

Re:Astrée Static Analyzer for C and C++ by ryao on Friday February 03, 2023 @01:12AM (#34637726)

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

https://github.com/NASA-SW-VnV/ikos

[ Parent | on HN ]

Re:Astrée Static Analyzer for C and C++ by quentinkent1 on Friday February 03, 2023 @01:57AM (#34637995)

Also Mathworks Polyspace Code Prover: https://mathworks.com/products/polyspace-code-prover.html

[ Parent | on HN ]

Re:Astrée Static Analyzer for C and C++ by sam_bristow on Friday February 03, 2023 @02:00AM (#34638024)

I _think_ Perforce's QA-C uses abstract interpretation, but I'm not 100% sure.

[ Parent | on HN ]

Re:Astrée Static Analyzer for C and C++ by edwcross on Friday February 03, 2023 @03:32AM (#34638731)

Also Frama-C/Eva: https://www.frama-c.com/fc-plugins/eva.html

[ Parent | on HN ]

Re:Astrée Static Analyzer for C and C++ by mdaniel on Friday February 03, 2023 @12:01PM (#34643963)

It 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 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

[ Parent | on HN ]

Re:Astrée Static Analyzer for C and C++ by mschnell on Friday February 03, 2023 @07:01AM (#34640051)

You can add grammatech‘s codesonar

[ Parent | on HN ]

Re:Astrée Static Analyzer for C and C++ by marmetio on Friday February 03, 2023 @11:08AM (#34642993)

I 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-compl...

[ Parent | on HN ]