Formal verification meets stochastic analysis

The thesis goal is to explore the relations between Formal Verification techniques in Computer Science and Stochastic Analysis in Mathematics. They both deal with probabilistic dynamical systems, implying that the number of connections is significant. The Formal Verification studies dynamical systems' properties, which are specified in terms of logic statements. This discipline has been successfully applied to multiple industry problems, such as ``verification of'' Software, Microprocessors or Neural Networks. The models studied have a countable states space and this can be considered the main obstacle to extend Formal Verification techniques for the computation of likelihoods in the case of Stochastic Differential Equations. However, the most studied properties in Formal Verification have a clear characterization in Mathematics. In this thesis, we focus on the safety property ``always'', which can be characterized as an exit time in the theory of Stochastic Analysis. The main difficulties are twofold. Firstly, if we are particularly interested in discretizing the states space - going from a continuous, uncountable space to a finite countable one - it is very likely to have an explosion of the cardinality of the states space. This leads to problems both in time and memory complexity. We find a new characterization of the barycenter of a discrete probability measure, which allows us to introduce a new algorithm for the recombination problem. Then, we use the algorithm to build recombining trees in order to approximate weakly stochastic processes, solving the exponential explosion of the cardinality of the states space. Secondly, one has to consider the approximation error: if the probability to exit from a safety region has not an analytical closed-form, a numerical scheme must be considered and therefore it is important to analyse the error. We introduce a grid-free approach for the computation of Probabilistic Safety Regions using Malliavin Calculus.