Formal Primal-Dual Algorithm Analysis
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914530197504000 |
|---|---|
| author | Abdulaziz, Mohammad Ammer, Thomas Madlener, Christoph |
| author_facet | Abdulaziz, Mohammad Ammer, Thomas Madlener, Christoph |
| contents | We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the Adwords algorithm, which models the assignment of search queries to advertisers in the context of search engines. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_20807 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Formal Primal-Dual Algorithm Analysis Abdulaziz, Mohammad Ammer, Thomas Madlener, Christoph Logic in Computer Science Discrete Mathematics Data Structures and Algorithms We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the Adwords algorithm, which models the assignment of search queries to advertisers in the context of search engines. |
| title | Formal Primal-Dual Algorithm Analysis |
| topic | Logic in Computer Science Discrete Mathematics Data Structures and Algorithms |
| url | https://arxiv.org/abs/2604.20807 |