LARA

Run-Time Monitoring

Take a program $M$ (infinite state) and automaton for specification $S$, and run both $M$ and $S$ in parallel. $S$ reports an error if it gets into a state from which it cannot reach an accepting state.

Advantage: works for infinite-state systems, and for very expressive specifications

Disadvantage: run-time checking only, we cannot tell anything about executions that the program did not experience.

See Monitoring oriented programming