The causality in synchronous languages is a very old problem, used to produce modular scheduled imperative code, for which many answers have already been given.
Interestingly, starting from a state-based semantics for a Lustre-like language, I will present how the causality could be used to ease the static analysis of this language.
After reducing the semantics of this language to the semantics of a simple equational language (forgetting every notion of stream or state), I will sketch several abstract domains which can be used to perform sound-by-construction causality analyses.
Finally, I will show how a reduced product of these domains can be used to get Zelus’ modular causality analysis.
If time permits, I will also present my ideas to extend this work to higher-order programs.
