Contraintes sur des flux appliquées a la vérification de programmes audio

National audience; La programmation par contraintes s'attaque en gé-néraì a desprobì emes statiques, sans notion de temps. Cependant, les méthodes de réduction de domaines pourraient par exemplê etre utiles dans desprobì emes portant sur des flux. C'est le cas de la vérification de programmes temps-réel, avec des variables dont les valeurs peuvent changer a chaque pas de temps. Dans cet article, nous nous intéressons a la vérification de domaines de variables (flux) dans le cadre d'un langage de diagrammes de blocs. Nous proposons une méthode de réduction de domaines de ces flux, pour encadrer finement les valeurs prises au cours du temps. En particulier, nous proposons un nouvel algorithme pour calculer un point fixe dans le cas des boucles temporelles. Nous présentons ensuite une application au langage FAUST, un langage fonctionnel temps réel pour le traitement audio et nous testons notre approche sur différents programmes FAUST standards. Abstract Constraint programming usually deals with static problems. However, domain reduction method could be useful in stream-based problems. This is the case in formal verification of real time programs for which variables can be assigned different values at every single time. In this paper, we focus on domain checking of stream variables in the context of block diagram languages. We propose a reduction algorithm for streams in order to tightly reduce their domains all over the time. Particularly , we propose a new technique to compute fix points of temporal loops. Finally, we apply our method to the FAUST language, which is a real time language for processing and generating audio streams. We also test some standards FAUST programs.