Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.10246 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _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 |