This is the web interface of SMCDEL 1.0.0, a symbolic model checker for Dynamic Epistemic Logic. See this paper and this technical report for more information.