AlanLight: sound, functionally correct, bounded acyclic data flow modeling

For programs controlling industrial processes, it is of vital importance that they produce results conform their functional specification. Furthermore, it is important that their running times are bounded, and that we can predict corresponding worst-case scenarios. Programs written in general purpose programming languages can crash or produce...