I beg to differ: there are a few tools which are comparable. Frama-C (https://www.frama-c.com https://www.frama-c.com) is an open source framework that has, am

I beg to differ: there are a few tools which are comparable. Frama-C (https://www.frama-c.com https://www.frama-c.com) is an open source framework that has, among its analyzers, one based on abstract interpretation (https://www.frama-c.com/fc-plugins/eva.html https://www.frama-c.com/fc-plugins/eva.html) that is very similar in spirit to Astree. MOPSA (https://mopsa.lip6.fr https://mopsa.lip6.fr) is another open-source project (albeit more recent, and in a more "academic" stage) that also provides abstract interpretation to analyze C programs for flaws. NASA also released IKOS (https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos), on the same vein. Of course they lack the polish of a product which costs tens of thousands of euros per license, but they are open source, and their purpose is the same: to ensure code safety via formal methods, in particular abstract interpretation. It is possible to get these tools to analyze some code and generate no complaints, which ensures absence of several kinds of problems, such as memory safety issues. Then again, it's hard to know exactly how much they differ from Astree, since you need a license to compare them, and I don't even know if you are allowed to publish such comparisons.