Small Bug, Big Bang
Title: Small Bug, Big Bang
Speaker: Jean-Jacques Lévy (INRIA,France and CAS,China)
Time: 11:00-12:00, 31st October 2013
Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
This talk is intended to precise a story usually vaguely described about the explosion of the first launch of the Ariane 5 rocket in July 1996 due to a software bug. I will present the work that we realized in our research-team at INRIA, which was considered as the first real application of static analysis for programs. Alain Deutsch used his fantastic alias analysizer IABC and Georges Gonthier performed as usual an incredible debugging analysis. This work was also contributed by my Inria colleagues: Damien Doligez, Robert Ehrlich, Francois Rouaix, Marcin Skubiszewski.
This talk is intended to precise a story usually vaguely described about the explosion of the first launch of the Ariane 5 rocket in July 1996 due to a software bug. I will present the work that we realized in our research-team at INRIA, which was considered as the first real application of static analysis for programs. Alain Deutsch used his fantastic alias analysizer IABC and Georges Gonthier performed as usual an incredible debugging analysis. This work was also contributed by my Inria colleagues: Damien Doligez, Robert Ehrlich, Francois Rouaix, Marcin Skubiszewski.
Biography:
See http://pauillac.inria.fr/~levy/bio.html
Summary: Graduated from Ecole polytechnique 1968, PhD at Paris 7 1978, senior researcher emeritus at Inria, Professor at Ecole polytechnique
1992-2006, Director of Microsoft Research-Inria Joint Centre 2006-2012. Worked in Operating Systems, Lambda Calculus, Term Rewriting Systems, Semantics of Distributed systems. Now in program verification with Coq and Why3.