Isabelle logo

Manuel Eberl

Chair for Logic and Verification

Verifying Randomised Social Choice

by Manuel Eberl

In: Proceedings of the 12th International Symposium on Frontiers of Combining Systems (Forthcoming)

Abstract:

This work describes the formalisation of a recent result from Randomised Social Choice Theory in Isabelle/HOL. The original result had been obtained through the use of linear programming, an unverified Java program, and SMT solvers; at the time that the formalisation effort began, no human-readable proof was available. Thus, the formalisation with Isabelle eventually served as both independent rigorous confirmation of the original result and led to human-readable proofs both in Isabelle and on paper.

This presentation focuses on the process of the formalisation itself, the domain-specific tooling that was developed for it in Isabelle, and how the structured human-readable proof was constructed from the SMT proof. It also briefly discusses how the formalisation uncovered a serious flaw in a second peer-reviewed publication.

Download preprint PDF (452 KiB)

BibTeX:

@inproceedings{eberl19rsc,
author="Eberl, Manuel",
title="Verifying Randomised Social Choice",
year="2019",
booktitle="Frontiers of Combining Systems"
}

Download BibTeX (153 Bytes)