Professor Wojciech Jamroga, from the Polish Academy of Sciences, presents a  seminar on How to Save Democracy (or Towards Model Checking of E-Voting Protocols in Alternating-time Temporal Logic).

Abstract: 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.


Bio: Wojciech Jamroga is a full 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 around 150 refereed publications, and has been a Program Committee member of most important conferences and workshops in AI and multi-agent systems. According to Google Scholar, his papers have been cited over 3100 times, and his H-index is 29. The research track of Prof. Jamroga 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.
His teaching record includes numerous courses at ESSLLI (European Summer School in Logic, Language and Information) and EASSS (European Agent Systems Summer School), a tutorial at ECAI (European Conference on AI), several courses at doctoral schools, and tutorials at IJCAI/ECAI 2022 and PRIMA 2022 -- all of them on formal methods for multi-agent systems.