|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 (french) 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.
He also participated in the Collaborative Research Initiatives on Automatic Differentiation entitled Operational Reverse Mode coordinated by Christèle Faure.
|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.
|2007:||New test approach for embedded applications. Software Engineering (Workshops) 2007: 127-136.|
|Static Verification of Dynamic Properties. SIGADA 2003. White paper.|
|1998:||ARIANE 5 - The Software Reliability Verification Process. DASIA 1998: 201-205.|
|1997:||On the Complexity of Escape Analysis. POPL 1997: 358-371.|
|1995:||Semantic models and abstract interpretation techniques for inductive data structures and pointers. PEPM 1995: 226-229.|
|1994:||Interprocedural May-Alias Analysis for Pointers: Beyond k-limiting. PLDI 1994: 230-241.|
|1992:||A Storeless Model of Aliasing and its Abstractions using Finite Representations of Right-Regular Equivalence Relations. ICCL 1992: 2-13.|
|1992:||Operational models of programming languages and representations of relations on regular languages with application to the static determination of dynamic aliasing properties of data. PhD thesis, University Paris VI, 1992.|
|1991:||An Operational Model of Strictness Properties and Its Abstractions (Extended Abstract). Functional Programming 1991: 82-99.|
|1990:||On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specifications. POPL 1990: 157-168.|
Back to Christèle Faure home page.