Preserving provability over GPU program optimizations with annotation-aware transformations

DOI10.1007/S10703-025-00480-7MaRDI QIDQ6887490zbMATH OpenFDO

Authors Ömer Şakar, Mohsen Safari, Marieke Huisman, Anton Wijs

Publication date 9 December 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10703-025-00480-7

zbMATH Keywords

optimizationGPUprogram transformationdeductive verificationannotation-awareness

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms
• A formally verified compiler back-end
• A self-certifying compilation framework for WebAssembly
• Automated verification of the parallel Bellman-Ford algorithm
• Automatic translation of FORTRAN programs to vector form
• BFS-based model checking of linear-time properties with an application on GPUs
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal verification of parallel stream compaction and summed-area table algorithms
• From Verification to Optimizations
• Permission accounting in separation logic
• Refinement of parallel algorithms down to LLVM
• The impact of program transformations on static program analysis
• Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• Viper: a verification infrastructure for permission-based reasoning

This page was built for publication: Preserving provability over GPU program optimizations with annotation-aware transformations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6887490)