Gale-Shapley Verified
This paper presents a detailed verification of the Gale-Shapley
algorithm for stable matching (or marriage). The verification proceeds
by stepwise transformation of programs and proofs. The initial steps
are on the level of imperative programs, ending in a linear time
algorithm. An executable functional program is obtained in a last
step. The emphasis is on the stepwise development of the algorithm and
the required invariants.
Springer
open access
Author pdf
BibTeX:
@article{Nipkow-JAR24,
author={Tobias Nipkow},
title={{Gale-Shapley} Verified},
journal={J. Automated Reasoning},volume={68},number={2},pages={12},year={2024}}
Isabelle theories in the
Archive of Formal Proofs