Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal
The design and implementation of an e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how the voting system works, and what requirements on the system are relevant. In this paper, we propose that the state-of-art model checker Uppaal provides a good environment for modelling and preliminary verification of voting protocols. To illustrate this, we present an Uppaal model of Pr\^et \`a Voter, together with some natural extensions. We also show how to verify a variant of receipt-freeness, despite the severe limitations of the property specification language in the model checker.
Code (0)
등록된 구현이 없습니다.
Tasks
modelSimilar Papers 제목 키워드 기반
Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC
Safe and interpretable sequential decision-making is critical in healthcare, yet reinforcement learning (RL) policies for sepsis treatment optimization remain opaque and difficult to verify. Standard probabilistic model …
Reinforcement LearningdtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts
Recent advances have shown how decision trees are apt data structures for concisely representing strategies (or controllers) satisfying various objectives. Moreover, they also make the strategy more explainable. The rece…
Decision MakingShow Me the Work: Fact-Checkers' Requirements for Explainable Automated Fact-Checking
The pervasiveness of large language models and generative AI in online media has amplified the need for effective automated fact-checking to assist fact-checkers in tackling the increasing volume and sophistication of mi…
Decision MakingFact CheckingMisinformationNeural spell-checker: Beyond words with synthetic data generation
Spell-checkers are valuable tools that enhance communication by identifying misspelled words in written texts. Recent improvements in deep learning, and in particular in large language models, have opened new opportuniti…
Language ModelingLanguage ModellingSynthetic Data GenerationExploring Multidimensional Checkworthiness: Designing AI-assisted Claim Prioritization for Human Fact-checkers
Given the massive volume of potentially false claims circulating online, claim prioritization is essential in allocating limited human resources available for fact-checking. In this study, we perceive claim prioritizatio…
Fact CheckingInformation Retrieval