Michael R. Lowry
In joint work with Cordell Green and with input from Barry Boehm, a model for software reliability versus software size was developed for NASA’s Mars Exploration Program. This analysis was summarized in a graph extrapolating the future likelihood of mission-critical software errors with increased software complexity. The graph helps to understand the various technologies and methods that can address this problem. This short paper then relates this to some of the early motivations for 'verifiably correct' program synthesis technology, and suggests the approach of a separate certification stage to address correctness.