Американскому космическому агенству приходится решать весьма непростые задачи создания надежного программного обеспечения. Специалисты NASA, занимающиеся полетами в глубокий космос, преодолевают очевидный кризис в разработке программного обеспечения, опираясь на два дополняющих друг друга подхода. Один уделяет первостепенное внимание программной инженерии, а второй использует потенциал автоматической генерации и провеки корректности кода.
