Robert Dewar
AdaCore

Safety critical programs require a comprehensive approach, that combines the use of specialized languages, such as SPARK, specialized tools, rigorously controlled testing, and the use of formal methods. In this paper, we survey the use of these techniques, and explain how they can be used to build error-free software systems. We also discuss how these techniques can be used in more general, non-safety-critical systems to improve reliability.