Gale-Shapley Verified

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Article number12
JournalJournal of Automated Reasoning
Volume68
Issue number2
DOIs
StatePublished - Jun 2024

Keywords

  • Gale-Shapley
  • Proof
  • Verification

Fingerprint

Dive into the research topics of 'Gale-Shapley Verified'. Together they form a unique fingerprint.

Cite this