About synchronous programming and abstract interpretation

This paper intends to highlight the connection between synchronous programming and abstract interpretation. First, the specific technique for compiling synchronous programs into interpreted automata can be seen as a partial evaluation. The second point concerns program verification. Most critical properties of reactive systems are safety properties, which can be translated into invariants, through the use of synchronous observers. Invariants can be proved by means of approximate reachability analysis, which is probably the most studied application of abstract interpretation.