On considère un système contrôlé linéaire en dimension finie, sous contraintes convexes compactes. Dans ce contexte, on s’intéresse à l’atteignabilité d’états cibles. À l’aide d’hyperplans supports, on introduit une fonctionnelle dont la positivité est équivalente à l’atteignabilité de la cible. On en déduit un schéma de preuve de non-atteignabilité assistée par ordinateur, passant par une discrétisation de cette fonctionnelle, la recherche d’un point négatif et l’estimation rigoureuse des erreurs de discrétisation et d’arrondis commises. Cette méthode est illustrée numériquement par divers théorèmes numériques sur plusieurs exemples, comprenant notamment des calculs de bornes inférieures de temps minimaux d’atteignabilité et des garanties de non-atteignabilité de zones dangereuses.