Inferring Safe Maude Programs with ÁTAME

In this paper, we present \atame, an assertion-based program specialization tool for the multi-paradigm language Maude. The program specializer \atame\ takes as input a set $\cA$ of system assertions that model the expected program behavior plus a Maude program $\cR$ to be specialized that might violate some of the assertions in $\cA$. The outcome of the tool is a safe program refinement $\cR'$ of $\cR$ in which every computation is a good run, i.e., it satisfies the assertions in $\cA$. The specialization technique encoded in $\atame$\ is fully automatic and ensures that no good run of $\cR$ is removed from $\cR'$, while the number of bad runs is reduced to zero. We demonstrate the tool capabilities by specializing an overly general nondeterministic dam controller to fulfill a safety policy given by a set of system assertions.