This year has been mainly devoted to the construction of a workbench to experiment about control structure refinements. The tool takes as input an implicit representation of an interpreted automaton, involving Boolean and numerical state variables, Boolean and numerical input variables. The transition function is defined by a system of equations, defining the next values of state variables, by means of Boolean and linear expressions. The automaton can be equiped with an assertion (restriction on inputs) and an invariant to be proved. Such an automaton can be made partially explicit, by distinguishing sets of states and specializing the transition function for each such set. The existing linear relation analysis can be applied both forward (reachable states) and backward (states possibly leading to the violation of the invariant). Some heuristics for the refinement of the explicit control structure have already been experimented.