  The safety of cyber-physical systems rests on the correctness of their
monitoring mechanisms. This is problematic if the specification of the monitor
is implemented manually or interpreted by unreliable software. We present a
verifying compiler that translates specifications given in the stream-based
monitoring language Lola to implementations in Rust. The generated code
contains verification annotations that enable the Viper toolkit to
automatically prove functional correctness, absence of memory faults, and
guaranteed termination. The compiler parallelizes the evaluation of different
streams in the monitor based on a dependency analysis of the specification. We
present encouraging experimental results obtained with monitor specifications
found in the literature. For every specification, our approach was able to
either produce a correctness proof or to uncover errors in the specification.

Software Engineering;Formal Languages and Automata Theory