ckfinite

27 seconds, compressed to 21 seconds for reasons of the song (the film was sped up). If you watch carefully, you can see the edit points where they are all grounded for the reset - the editor deserves a big hand of applause!

Will InSight be using any of the new EDL GNC techniques proposed for Mars 2020, like terrain-relative navigation or optimal powered descent guidance?

How do you validate software correctness? Do you use formal verification, and how do you specify correctness? How tight are the real-time requirements for the flight software?

Thanks a lot for coming and talking about your work!

• How do you do trajectory optimization? Are you using an open loop or closed loop guidance system, and do you use an integrated attitude control approach or treat them as separate problems?

• Do you use formal verification for source code? It's common, at least in aircraft companies, to formally verify the key source to exclude edge cases like the ones you mention not being able to test for.

• Edit: What kind of hardware do you fly? Are you using commodity systems, or specially space-rated ones, and what operating systems do they use?