Student research opportunities
Reasoning About Voting Schemes
Project Code: CECS_1161
This project is available at the following levels:
Honours, Summer Scholar
Please note that this project is only for undergraduate students.
Keywords:
Model Checking, Voting Schemes
Supervisor:
Dr Peter BaumgartnerOutline:
Fitzroy is a model-checker for the logic CTL* over fragments of first-order logic. Unlike most other systems, it supports modelling of states with a rich structure using lists, arrays and records and first-order logic. Fitzroy is implemented in Scala.
Goals of this project
This is an application project. The project asks to formalize certain (simple) voting schemes in first-order logic and trying to prove or disprove their correctness by automated theorem provers.
Student Gain
Learning to formalize problems in logic and applying automated reasoning tools to them
