Formal methods for dynamical systems: invariants, reachability, inference.

This thesis is centered on Formal Methods for dynamical systems. In particular, we focus on continuous dynamical systems specified by systems of ordinary differential equations (ODEs). We first consider the task of finding invariants, which are useful in the Safety analysis of systems. We focus on a particular type of invariants, conservation laws. We present a method to compute all the polynomial conservation laws up to a specified order of derivatives and degree for systems of partial differential equations (PDEs). The method is based only on the definition of conservation law and on linear algebraic computations. We then study conditions and methods to compute reduced linear approximations of nonlinear ordinary differential equations (ODEs) that are accurate also non locally, and present an algorithm that, given an initial set and a finite time horizon, builds a tight overapproximation of the set of its reachable states (reachset) at specified times, relying on Carleman linearization and Krylov projection. Next, we consider stream differential equations (SDEs), a generalization of differential equations in the framework of stream calculus, that is centered on the manipulations of infinite sequences of scalars from a field, or streams. Working within this framework, we provide a method to find all polynomial invariants that fit in a user specified polynomial template, for a given SDE-based initial value problem. We also establish a stream version of Implicit Function Theorem (IFT) for systems of stream polynomial equations, and show the advantages of the stream IFT with respect to the classical IFT from a computational point of view. We then consider parametric ODEs systems. We introduce an algorithm to compute guaranteed estimates of posterior expectations for the parameters from given observations. We work in a general model, where the relation between observations and parameters is a function, with additive noise; the function can be, in particular, the solution of a ODE. The algorithm relies on a combination of methods based on uncertain probability, Interval Arithmetic and Monte Carlo simulation. Guarantees come in the form of confidence intervals. Finally, we consider a more general and flexible approach to parameter inference based on Probabilistic Programming. In particular, we present an action-based probabilistic programming language equipped with a small-step operational semantics, where discrete and continuous distributions can be freely mixed and unbounded loops are allowed. Our semantics directly leads to an exact sampling algorithm that can be efficiently SIMD-parallelized.