% vim: set spelllang=nl:
\begin{abstract}
	We beschrijven een manier om de semantiek van Smurf \cite{safalra} formeel te
	specificeren, om het makkelijker te maken over de taal te redeneren. Smurf is
	interessant, omdat het een commando heeft om een string als Smurfprogramma
	uit te voeren. Vervolgens laten we zien hoe de semantiek gebruikt kan worden
	om over de taal te redeneren. Hiervoor introduceren we de tool
	\emph{CleanSmurf}~\cite{cleansmurf}, een bewijshulp voor Smurf.
\end{abstract}