CMU Silicon Valley welcomes Gerard Holzmann
Date/Time: Tuesday, October 27, 2015 1:30 pm (PT) / 4:30 pm (ET)
Location: CMU Silicon Valley Campus: Bldg 23, Rm 118
Source: Gerard Holzmann
Computer Scientist and Researcher at Bell Labs and NASA
Proof or Consequences
Apart from death and taxes, there are a few other sobering facts of life. One such fact is that software always seems to grow with time. Another is that the number of undiscovered software defects in applications also tends to grow, as software packages gradually become more complex and start supporting more and more features. Most disturbing, perhaps, is that all software of any practical significance is likely to have more undiscovered than discovered defects. So what can we do when the reliability of the software we write is really important?
In his lecture, Dr. Holzmann will summarize what steps NASA Jet Propulsion Laboratory's flight software team took to prevent defects from finding their way into the code for the Mars Science Laboratory mission, that safely landed a large rover onto the surface of Mars in August 2012.
He will also talk in some detail about a methodology we are developing to efficiently analyze implementation level multi-threaded C source code for logical correctness properties specified in linear temporal logic.
Gerard J. Holzmann is a JPL Fellow and Senior Research Scientist. He leads the JPL Laboratory for Reliable Software. Gerard obtained his Ph.D. in 1979 from