Properties of coercion resistance and voter verifiability refer to the existence of an appropriate strategy for the voter, the coercer, or both. One can try to specify such properties by formulae of a suitable strategic logic. However, automated verification of strategic properties is notoriously hard, and novel techniques are needed to overcome the complexity.

I will start with an overview of the relevant properties, show how they can be specified, and present some new results for model checking of strategic properties.

Wojtek Jamroga is an associate professor at the Polish Academy of Sciences and a research scientist at the University of Luxembourg. His research focuses on modeling, specification and verification of interaction between agents. He has coauthored over 100 refereed publications, and has been a Program Committee member of most important conferences and workshops in AI and multi-agent systems. His research track includes the Best Paper Award at the main conference on electronic voting (E-VOTE-ID) in 2016, and a Best Paper Nomination at the main multi-agent systems conference (AAMAS) in 2018.