Résumé
Au cours de son exposé, François Pottier a montré qu'une logique de programmes permet non seulement d'établir la correction d'un programme, mais aussi de contrôler le nombre d'opérations qu'il effectue, et donc, indirectement, son temps de calcul.
Il a expliqué comment ce comptage peut se faire d'abord en logique de Hoare, puis en logique de séparation, où le comptage du temps peut s'effectuer de façon plus décentralisée, et où des artifices comptables très élaborés peuvent être mis en place par l'utilisateur.
