What every C Programmer should know about undefined behavior #2/3
Posted May 18, 2011 0:34 UTC (Wed) by price
In reply to: What every C Programmer should know about undefined behavior #2/3
Parent article: What every C Programmer should know about undefined behavior #2/3
> Polyspace is commercial and not developed in academia.
Wrong. It is commercial, but it came from academia.
Quick history of Polyspace, unfortunately quoting an obituary (http://christele.faure.pagesperso-orange.fr/AlainDeutsch.html - see original for many links):
- 1992-1993: Alain obtained his PhD on static analysis by abstract interpretation for dynamic data structures with pointers.
He made a post-doc at the University of Carnegie-Mellon on the static analysis of communication protocols.
- 1993-1996: Alain joined PARA/INRIA Rocquencourt. He focussed on the static analysis of programs and developed the IABC analyser based on abstract interpretation.
- 1996-1999: He specialized his IABC analyzer to runtime error detection in Ada source code and proved the effectiveness of static analysis by exhibiting code errors in the flight programme of Ariane 5 incriminated in the flight 501 crash.
Alain was a member of the qualification board of flight 502, which gave the green light for the second (successful) launch of Ariane 5. ...
- 1999-2006: He founded PolySpace Technologies together with Daniel Pilaud and became the Technical Director (Chief Technical Officer).
PolySpace Technologies industrialized his IABC analyzer for Ada source code, extended it to C C++ Ada95 and commercialized PolySpace Verifier for Ada83, C, C++, Ada95.
So the tool was developed by a PhD researcher working at a research lab (and well-known hotbed of static type systems), refined for several years, and finally commercialized by him and others.
Another static analysis tool widely used in practice is Coverity -- that one came from a bunch of academics at Stanford. That's the usual story for this kind of tool.
to post comments)