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

Gerard Holzmann

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 Delft University of Technology in The Netherlands. Before joining JPL, he was a computing science researcher in the Unix group at Bell Laboratories in Murray Hill, NJ. Holzmann is best known for designing and building the widely used Spin model checker and the winner of 2001 ACM Software System Award.