> In contrast, thanks to its modularity and domain-awareness, Astrée can be made exceptionally precise, often to the point of producing 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.