Proof or Consequences

Gerard Holzmann, Ph.D.
Founder, Nimble Research (http://nimbleresearch.com/)

Please join us for the fifth of the Orange County ACM Chapter's 2017 bi-monthly evening program series.

Agenda

6:30 PM Doors Open & Networking

7:00 PM Announcements and Presentation

8:30 PM Meeting Adjourned

Event Details

All software of any practical significance is likely to have residual defects. How can we reduce those number to a minimum when we're developing really critical code?

I'll first summarize what steps we took in JPL's flight software team to prevent as many defects as possible from finding their way into the roughly 3 million lines of mission critical code that was developed for the Mars Science Lab Curiosity Rover that has been exploring the surface of Mars for almost five years now.

I'll then talk briefly also about an experimental new methodology that can allow us to analyze multi-threaded C source code more thoroughly for compliance with logical correctness properties that are expressed in linear temporal logic.

Speaker Bio

Dr. Holzmann is the founder and a researcher at Nimble Research and a Visiting Associate in Computing & Mathematical Sciences at the California Institute of Technology. He recently retired from NASA's Jet Propulsion Laboratory, where he was the founder and leader of JPL's Laboratory for Reliable Software (http://lars-lab.jpl.nasa.gov/). Prior to joining JPL, he was a researcher at Bell Labs.

He has designed and built software for image editing (Pico 1983), logic model checking (Spin 1998), static code analysis (Uno 2002, Cobra 2016), and for peer code review (Scrub 2009). He was a member of the flight software team for NASA's Mars Science Laboratory Mission[masked],

He is a Fellow of the ACM and member of the US National Academy of Engineering. He is the recipient of the ACM System Software Award (2001), the ACM SIGSOFT Outstanding Research Award (2002), the Edison Patent Award (2003), co-recipient of the ACM Kannellakis Award (2006), recipient of an Honorary Doctorate from Twente University (2006), the NASA Exceptional Engineering Achievement Medal (2012) and the IEEE Harlan D. Mills Award (2015).

He earned his B.Sc., M.Sc. and Ph.D degrees at Delft University of Technology, The Netherlands.

Co-sponsors

This event is co-sponsored by the IEEE Orange County Computer Society.