Abstract
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.
Original language | English |
---|---|
Article number | 12 |
Journal | Journal of Automated Reasoning |
Volume | 68 |
Issue number | 2 |
DOIs | |
State | Published - Jun 2024 |
Keywords
- Gale-Shapley
- Proof
- Verification