Unlike dynamic analysis--such as testing--where results are valid only for those paths actually executed, static analysis has the advantage that it considers all possible executions. It does this using symbolic execution and automated deduction. Thanks to recent advances in these fields, static analysis has become a powerful and practical tool for bug finding and for certain kinds of assurance.

There are tradeoffs in static analysis between the strength of properties examined, the numbers of false alarms, the guarantees that can be provided, and the amount of annotation and other guidance that must be supplied by the user. Commercial vendors of static analysis tools make these tradeoffs in ways that best suit their overall market, although users with specific needs might wish for different choices.

I will provide an introduction to some of the techniques employed in static analysis, and an overview of issues in its application to assurance for complex medical devices.