Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908484146036736 |
|---|---|
| author | Stevens, Lukas Ghidini, Rebecca |
| author_facet | Stevens, Lukas Ghidini, Rebecca |
| contents | Using Isabelle/HOL, we verify a union-find data structure with an explain operation due to Nieuwenhuis and Oliveras. We devise a simpler, more naive version of the explain operation whose soundness and completeness is easy to verify. Then, we prove the original formulation of the explain operation to be equal to our version. Finally, we refine this data structure to Imperative HOL, enabling us to export efficient imperative code. The formalisation provides a stepping stone towards the verification of proof-producing congruence closure algorithms which are a core ingredient of Satisfiability Modulo Theories (SMT) solvers. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_10246 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm Stevens, Lukas Ghidini, Rebecca Logic in Computer Science Using Isabelle/HOL, we verify a union-find data structure with an explain operation due to Nieuwenhuis and Oliveras. We devise a simpler, more naive version of the explain operation whose soundness and completeness is easy to verify. Then, we prove the original formulation of the explain operation to be equal to our version. Finally, we refine this data structure to Imperative HOL, enabling us to export efficient imperative code. The formalisation provides a stepping stone towards the verification of proof-producing congruence closure algorithms which are a core ingredient of Satisfiability Modulo Theories (SMT) solvers. |
| title | Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.10246 |