Abstract. We present the automatic verification of time-bounded properties of programs written in the reactive language Electre. For this, Electre programs are translated into so-called stopwatch automata, automata with chronometers to measure time. Properties are expressed in the logic TCTL and model-checking algorithms are used to verify those properties on Electre stopwtach automata. We show that bounded TCTL is decidable on stopwatch automata.