Résumé | Depuis une dizaine d'années, les techniques d'optimisation
sous-contraintes (LP, SDP, SOS...) apparaissent en vérification de programmes
numériques par analyse statique.
Dans ma présentation, je montrerai comment générer des modèles
utilisant ces techniques pour prouver automatiquement des propriétés
sur des programmes numériques grâce à leur représentation par des
systèmes dynamiques à temps discret.
|