Note that Astrée was developed in France, by researchers from Inria. AbsInt sells it packaged as a product (with support, etc), but the bulk of the research was done in the 2000's by researchers such as Cousot.
This is also the case with CompCert, which is still developed mostly by French researchers (with an open-source, non-commercial license), and packaged in commercial form by AbsInt.
Ah, good to know (and I guess this explains the accent aigu :)). Well, there's a lot of excellent CS research in France, too - and nice to see there's a collaboration (the French border is just around the corner from Saarbrücken).
> The company name is an acronym for “abstract interpretation”, a sophisticated approach to static program analysis formalized by Patrick and Radhia Cousot at the Laboratoire d’Informatique, Grenoble in 1977. It is by implementing this approach that we were able to develop our unique, highly successful products.
This is also the case with CompCert, which is still developed mostly by French researchers (with an open-source, non-commercial license), and packaged in commercial form by AbsInt.