Synthesising Correct Concurrent Runtime Monitors in Erlang
Adrian Francalanza, Aldrin Seychell · 2013
Abstract. We study the correctness of automated synthesis for concurrent mon-itors. We adapt HML, a subset of the Hennessy-Milner logic with recursion, to specify safety properties of Erlang programs, and define an automated transla-tion from HML formulas to Erlang monitors so as to detect formula violations at runtime. We then formalise monitor correctness for our concurrent setting and describe a technique that allows us to prove monitor correctness in stages; this technique is used to prove the correctness of our automated monitor synthesis.