A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
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_ | 1866911193530105856 |
|---|---|
| author | Kohlen, Bram Schäffeler, Maximilian Abdulaziz, Mohammad Hartmanns, Arnd Lammich, Peter |
| author_facet | Kohlen, Bram Schäffeler, Maximilian Abdulaziz, Mohammad Hartmanns, Arnd Lammich, Peter |
| contents | We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM that is based on floating-point arithmetic. We use the Isabelle/HOL proof assistant to verify convergence of our abstract definition of interval iteration and employ step-wise refinement to derive an efficient implementation in LLVM code. To that end, we extend the Isabelle Refinement Framework with support for reasoning about floating-point arithmetic and directed rounding modes. We experimentally demonstrate that the verified implementation is competitive with state-of-the-art tools for MDPs, while providing formal guarantees on the correctness of the results. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_10127 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs Kohlen, Bram Schäffeler, Maximilian Abdulaziz, Mohammad Hartmanns, Arnd Lammich, Peter Logic in Computer Science We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM that is based on floating-point arithmetic. We use the Isabelle/HOL proof assistant to verify convergence of our abstract definition of interval iteration and employ step-wise refinement to derive an efficient implementation in LLVM code. To that end, we extend the Isabelle Refinement Framework with support for reasoning about floating-point arithmetic and directed rounding modes. We experimentally demonstrate that the verified implementation is competitive with state-of-the-art tools for MDPs, while providing formal guarantees on the correctness of the results. |
| title | A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2501.10127 |