The DOI displayed above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
DOI: 10.4121/bf0fef24-4f0f-4de6-a58d-07b9ba601804

Kohlen, Bram; Schäffeler, Maximilian; Abdulaziz, Mohammad; Hartmanns, Arnd; Peter Lammich (2025): Artifact for the paper "A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs". Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/bf0fef24-4f0f-4de6-a58d-07b9ba601804.v1

Categories

• Computer Software
• Computation Theory and Mathematics
• Information and Computing Sciences

Keywords

Correct-by-construction Floating-point IEEE 754 Interactive Theorem Proving Interval Iteration LLVM Markov Decision Process Probabilistic Model Checking Software Verification

Licence

BSD-3-Clause

Export as...

RefWorks BibTeX Reference Manager Endnote DataCite NLM DC CFF

by Bram Kohlen , Maximilian Schäffeler , Mohammad Abdulaziz , Arnd Hartmanns , Peter Lammich

This artifact contains the proofs of correctness of an algorithm for Interval Iteration (II) as well as a modified version of mcsta from the Modest Toolset with models to reproduce the benchmarks. The high-level proofs are described in the paper “A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs” accepted at CAV 2025. The proof is divided into a correctness proof for the abstract algorithm, a proof of correctness for the different data structures and a refinement to LLVM that is done using the Isabelle Refinement Framework. Running the proofs yields an LLVM implementation of the II algorithm. Once compiled into a library, it can directly be used by our modified version of mcsta to reproduce the experiments in our paper. To streamline the process, we have provided small scripts that perform basic tasks automatically (e.g. copying, moving, removing files and running mcsta).

This artifact is designed to run on a 64-bit Linux distribution (Docker available) with at least 32GB of RAM. Note that support of the AVX512 instruction set is a must to reproduce the benchmarks!

History

• 2025-04-11 first online, published, posted

Publisher

4TU.ResearchData

References

• https://doi.org/10.48550/arXiv.2501.10127

Funding

• NWO Open Competition OCENW.KLEIN.311: Verified Probabilistic Verification
• MISSION (grant code 101008233) [more info...] European Union's Horizon 2020 research and innovation programme under Marie Sk{\l}odowska-Curie grant agreement
• The Interreg North Sea project STORM_SAFE [more info...]
• Trustworthy Analysis of Stochastic Timed Systems (TruSTy) (grant code NWO VIDI grant VI.Vidi.223.110) [more info...] NWO
• VESPA: Verified, Efficient, and Secure Parallel Algorithms (grant code OCENW.M.21.291) [more info...] NWO
• ConVeY (grant code 378803395) Deutsche Forschungs- gemeinschaft

Organizations

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools (FMT);
Technische Universität München, Chair for Logic and Verification