Industrial strength exception freedom

Ada is unique amongst modern high-level languages in the degree to which it allows programming errors to be trapped at the compilation stage. Using a tool like the SPARK Examiner amplifies this effect and can provide a high degree of confidence that a program is well formed before we try and verify that its behaviour is correct. Despite this progress a less tractable class of errors remain: run-time exceptions. For safety-related systems a run-time error may be just as hazardous as any other logical error. For secure systems, guarding against the deliberate generation of such errors-through buffer overflow attacks for example-is vital. The paper explains how automated techniques based on formal verification or proof techniques have now matured and provide an industrial strength solution.