> In contrast, thanks to its modularity and domain-awareness, Astrée can be made exceptionally precise, often to the point of pro­ducing exactly zero false alarms.

I will guess that when analyzing avionics code with no memory allocation it is perfect, and when analyzing other code it is merely great. I wonder what the recruiting pipeline from INRIA into AbsInt is like.

On this kind of analysis, it strongly depends on the features that are used in the analyzed code and its degree of complexity. An analysis that is entirely automatic, detect every mistake and only mistakes is not possible in the general case.