This talk is about verified numerical algorithms in Isabelle/HOL, with a focus on guaranteed enclosures for solutions of ODEs. The enclosures are represented by zonotopes, arising from the use of affine arithmetic. Enclosures for solutions of ODEs are computed by set-based variants of the well-known Runge-Kutta methods.
All of the algorithms are formally verified with respect to a formalization of ODEs in Isabelle/HOL: The correctness proofs are carried out for abstract algorithms, which are specified in terms of real numbers and sets. These abstract algorithms are automatically refined towards executable specifications based on lists, zonotopes, and software floating point numbers. Optimizations for low-dimensional, nonlinear dynamics allow for an application highlight: the computation of an accurate enclosure for the Lorenz attractor. This contributes to an important proof that originally relied on non-verified numerical computations.[-]

Nous confions à nos ordinateurs de nombreux calculs mais la machine a des limites due à son arithmétique dite à virgule flottante. D'une part chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. D'autre part, les valeurs que l'ordinateur appréhende ont des limites vers l'infiniment petit et l'infiniment grand. Hors de ces bornes, l'ordinateur produit des valeurs spéciales souvent inattendues. La première partie de cet exposé montrera que l'ordinateur n'est pas infaillible ou plutôt que son utilisation est parfois abusive. La seconde partie consisitera en une utilisation judicieuse de l'arithmétique flottante de façon à récupérer les erreurs ou à garantir un calcul
presque juste, même dans les cas pathologiques.[-]

Robotic design involves modeling the behavior of a robot mechanism when it moves along potential paths set by the users. In this lecture, we will first give an overview of different approaches to design a set of kinematic equations associated with a robot mechanism. In particular, these equations can be used to solve the forward and the backward kinematics problems associated with a robot mechanism or to model its singularity locus. Then we will review methods to solve those equations, and notably methods to draw with guarantees the real solutions of an under-constrained system of equations modeling the singularities of a robot.[-]

Robotic design involves modeling the behavior of a robot mechanism when it moves along potential paths set by the users. In this lecture, we will first give an overview of different approaches to design a set of kinematic equations associated with a robot mechanism. In particular, these equations can be used to solve the forward and the backward kinematics problems associated with a robot mechanism or to model its singularity locus. Then we will review methods to solve those equations, and notably methods to draw with guarantees the real solutions of an under-constrained system of equations modeling the singularities of a robot.[-]