Formal verification of multi-agent systems is hard, both theoretically
and in practice. In particular, studies that use a single verification
technique typically show limited efficiency, and allow to verify only
toy examples. Here, we propose some new techniques and combine them
with several recently developed ones to see what progress can be
achieved for a real-life scenario. Namely, we use fixpoint
approximation, domination-based strategy search, partial order
reduction, and parallelization to verify heterogeneous scalable models
of the Selene e-voting protocol. The experimental results show that
the combination allows to verify requirements for much more
sophisticated models than previously.
