Abstract
The great strength of formal methods is that they allow consideration of all possible behaviors, and this could be of immense value in certification. However, automated formal analysis of large and complex artifacts is computationally infeasible, so compromises have to be made. These include use of interactive human guidance rather than full automation, analysis of models and abstractions rather than the real artifact, and analysis of weak properties (e.g., by static analysis) rather than full requirements. I will consider how these and other practical limitations affect the potential role of formal methods in certification. I will also outline weaknesses in current standards-based approaches to certification and sketch how multi-legged safety cases might provide a way to incorporate formal methods into certification processes.
