Invited Speakers

Electronic voting aims at guaranteeing apparently conflicting properties: no one should know how I voted and yet, I should be able to check that my vote has been properly counted. Many more properties may be considered such as everlasting privacy, coercion-resistance, or accountability. In this talk, we will first survey how voting protocols work through the example of the French Legislative elections in 2022.

Electronic voting belongs to the large family of security protocols, that aim at securing communications against powerful adversaries that may read, block, and modify messages. Many techniques and tools have been developed to formally prove the security of protocols. Yet, voting protocols push such techniques at their limits. We will see how to model and analyze the security of voting protocols using formal methods and in particular with the tool ProVerif, in order to (automatically) detect attacks at an early stage, or to prove security, yielding a better understanding of the security guarantees and the threat model.

Petri net research often builds on the definition of formal properties and corresponding analysis methods. A larger share of Petri net papers provides such formal contributions, but there are also works that offer empirical insights. Such empirical insights can be highly effective in stimulating major breakthroughs even in more formal areas of computer science, such as graph algorithms or automatic image recognition. In this paper, we discuss the benefits and challenges of complementing formal research on Petri nets with an empirical research agenda. To that end, we build on a methodological framework for algorithm engineering and present selected examples of empirical works on Petri nets. These examples illustrate the spectrum of potential contributions and emphasize the salience of validity concerns. These works can serve as pillars for advancing empirical research on Petri nets.