Uncertainties occur in different forms: data may be noisy, mechanisms may be inherently randomised, the visibility (of e.g. a robot) may not be optimal, and the environment in which a system needs to operate may behave in an unknown manner.

The central question that we will address is «Can we guarantee that AI systems are safe and dependable in the presence of such uncertainty?» We advocate using model-based, formal verification and synthesis with a particular focus on automation.

We will present techniques to verify uncertainty aspects modeled as randomness and to use formal synthesis to complete partial designs. Several example AI systems will illustrate the capabilities of these approaches.