Cover Image

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Kohlen, Bram, Schäffeler, Maximilian, Abdulaziz, Mohammad, Hartmanns, Arnd, Lammich, Peter
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formally Verified Approximate Policy Iteration
by: Schäffeler, Maximilian, et al.
Published: (2024)

Fixed Point Certificates for Reachability and Expected Rewards in MDPs
by: Chatterjee, Krishnendu, et al.
Published: (2025)

DTMC Model Checking by Path Abstraction Revisited (extended version)
by: Hartmanns, Arnd, et al.
Published: (2025)

Formally Verified Certification of Unsolvability of Temporal Planning Problems
by: Wang, David, et al.
Published: (2025)

Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
by: Budde, Carlos E., et al.
Published: (2024)

Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)
by: D'Argenio, Pedro R., et al.
Published: (2025)

Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality (extended version)
by: Budde, Carlos E., et al.
Published: (2025)

Time-Sensitive Importance Splitting
by: Dengler, Gabriel, et al.
Published: (2025)

A Formal Analysis of Capacity Scaling Algorithms for Minimum-Cost Flows
by: Abdulaziz, Mohammad, et al.
Published: (2026)

Verifying Floating-Point Programs in Stainless
by: Gilot, Andrea, et al.
Published: (2026)

Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
by: Mohanty, Hansa, et al.
Published: (2025)

Probabilistic Verification for Modular Network-on-Chip Systems (extended version)
by: Waddoups, Nick, et al.
Published: (2025)

Formal Primal-Dual Algorithm Analysis
by: Abdulaziz, Mohammad, et al.
Published: (2026)

parSAT: Parallel Solving of Floating-Point Satisfiability
by: Krahl, Markus, et al.
Published: (2025)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

A Formally Verified Lightning Network
by: Fabiański, Grzegorz, et al.
Published: (2025)

Formally Verified Animation for RoboChart using Interaction Trees
by: Ye, Kangfeng, et al.
Published: (2023)

Verified and Optimized Implementation of Orthologic Proof Search
by: Guilloud, Simon, et al.
Published: (2025)

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
by: Dvorak, Martin, et al.
Published: (2025)

Tractable Hyperproperties for MDPs
by: Gerlach, Lina, et al.
Published: (2026)

IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes
by: Mathiesen, Frederik Baymler, et al.
Published: (2024)

A Formal Correctness Proof of Edmonds' Blossom Shrinking Algorithm
by: Abdulaziz, Mohammad, et al.
Published: (2024)

Four Formal Models of IEEE 1394 Link Layer
by: Garavel, Hubert, et al.
Published: (2024)

Automatic Verification of Floating-Point Accumulation Networks
by: Zhang, David K., et al.
Published: (2025)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
by: Bryce, Aaron, et al.
Published: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

Towards Verifying Exact Conditions for Implementations of Density Functional Approximations
by: Helal, Sameerah, et al.
Published: (2024)

Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
by: Kappelmann, Kevin, et al.
Published: (2025)

Small Decision Trees for MDPs with Deductive Synthesis
by: Andriushchenko, Roman, et al.
Published: (2025)

Multi-Environment MDPs with Prior and Universal Semantics
by: Bordais, Benjamin, et al.
Published: (2026)

Decisiveness for countable MDPs and insights for NPLCSs and POMDPs
by: Bertrand, Nathalie, et al.
Published: (2020)

Formal Verification of the Safegcd Implementation
by: O'Connor, Russell, et al.
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

Certified Knowledge Compilation with Application to Formally Verified Model Counting
by: Bryant, Randal E., et al.
Published: (2025)

Omega-regular Verification and Control for Distributional Specifications in MDPs
by: Akshay, S., et al.
Published: (2025)

The Value Problem for Multiple-Environment MDPs with Parity Objective
by: Chatterjee, Krishnendu, et al.
Published: (2025)

Compositional Verification of Almost-Sure Büchi Objectives in MDPs
by: van der Vegt, Marck, et al.
Published: (2025)

Policies Grow on Trees: Model Checking Families of MDPs
by: Andriushchenko, Roman, et al.
Published: (2024)

Robust Almost-Sure Reachability in Multi-Environment MDPs
by: van der Vegt, Marck, et al.
Published: (2023)