Abstract FR:

Signal est un langage synchrone, a flots de donnees, destine a la specification de systemes reactifs et temps-reel. Cette these etudie des methodes et outils de preuve de programmes signal. Un codage polynomial, dans le corps des entiers modulo trois, decrit les aspects logiques et temporels des programmes; demontrer une propriete d'un systeme reactif consiste a verifier, au moyen d'outils de calcul formel, une propriete algebrique equivalente. La representation des fonctions polynomiales par graphes de decision ternaires permet une mise en uvre efficace de ces calculs