Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • HotDep '12 Home
  • Organizers
  • Registration Information
  • Workshop Program
  • Hotel and Travel Information
  • Sponsorship
  • Students
  • Help Promote
  • For Participants
  • Call for Papers
  • Past HotDeps

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Mars Code
Tweet

connect with us

http://twitter.com/usenix
https://www.facebook.com/events/225273080901144/

Mars Code

Authors: 

Gerard Holzmann, JPL Laboratory for Reliable Software

Abstract: 

On August 5 at 10:18 p.m. PDT, a large rover named Curiosity made a soft landing on the surface of Mars. Given the one-way light-time to Mars, the controllers on Earth learned about the successful touchdown 14 minutes later, at 10:32 p.m. PDT. As can be expected, all functions on the rover, and on the spacecraft that brought it to Mars, are controlled by software. In this talk we review the process that was followed to secure the reliability of this code.
Gerard Holzmann is a senior research scientist and a fellow at NASA's Jet Propulsion Laboratory, the lab responsible for the design of the Mars Science Laboratory Mission to Mars and its Curiosity Rover. He is best known for designing the Logic Model Checker Spin, a broadly used tool for the logic verification of multi-threaded software systems. Holzmann is a fellow of the ACM and a member of the National Academy of Engineering.

Gerard Holzmann, JPL Laboratory for Reliable Software

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@conference {255631,
author = {Gerard Holzmann},
title = {Mars Code},
year = {2012},
address = {Hollywood, CA},
publisher = {{USENIX} Association},
month = oct,
}
Download

Presentation Video

Presentation Audio

MP3 Download OGG Download

Download Audio

  • Log in or    Register to post comments

© USENIX

  • Privacy Policy
  • Conference Policies
  • Contact Us