[{"type":"chapter","title":"An Introduction to Voting Rule Verification","issued":{"date-parts":[["2017"]]},"page":"269\u2013287","container-title":"Trends in Computational Social Choice. Ed by.: Ulle Endriss","author":[{"family":"Beckert","given":"Bernhard"},{"family":"Bormer","given":"Thorsten"},{"family":"Gor\u00e9","given":"Rajeev"},{"family":"Kirsten","given":"Michael"},{"family":"Sch\u00fcrmann","given":"Carsten"}],"publisher":"AI Access","ISBN":"978-1-32691-209-3","abstract":"We give an introduction to deductive verification methods that can be used to\r\nformally prove that voting rules and their implementations satisfy specified\r\nproperties and conform to the desired democratic principles.\r\n\r\nIn the first part of the paper we explain the basic principles: We describe\r\nhow first-order logic with theories can be used to formalise the desired\r\nproperties. We explain the difference between (1) proving that one\r\nset of properties implies another property, (2) proving that a voting rule\r\nimplementation has a certain property, and (3) proving that a voting rule\r\nimplementation is a refinement of an executable specification. And we explain\r\nthe different technologies: (1) SMT-based testing, (2) bounded program\r\nverification, (3) relational program verification, and (4) symmetry breaking.\r\nIn this first part of the paper, we also explain the difference between\r\nverifying functional and relational properties (such as symmetries).\r\n\r\nIn the second part, we present case studies, including (1) the specification\r\nand verification of semantic properties for an STV rule used for electing the\r\nboard of trustees for a major international conference and (2) the\r\ndeduction-based computation of election margins for the Danish national\r\nparliamentary elections.","kit-publication-id":"1000092710"}]