  We consider the problem of under and over-approximating the image of general
vector-valued functions over bounded sets, and apply the proposed solution to
the estimation of reachable sets of uncertain non-linear discrete-time
dynamical systems. Such a combination of under and over-approximations is very
valuable for the verification of properties of embedded and cyber-physical
controlled systems. Over-approximations prove properties correct, while
under-approximations can be used for falsification. Coupled, they provide a
measure of the conservatism of the analysis. This work introduces a general
framework relying on computations of robust ranges of vector-valued functions.
This framework allows us to extend for under-approximation many precision
refinements that are classically used for over-approximations, such as affine
approximations, Taylor models, quadrature formulae and preconditioning methods.
We end by evaluating the efficiency and precision of our approach, focusing on
the application to the analysis of discrete-time dynamical systems with inputs
and disturbances, on different examples from the literature.
