Extending Contract Verification for Parallel Programming Models to Fortran
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913054610948096 |
|---|---|
| author | Oraji, Yussur Mustafa Bischof, Christian |
| author_facet | Oraji, Yussur Mustafa Bischof, Christian |
| contents | High-performance computing often relies on parallel programming models such as MPI for distributed-memory systems. While powerful, these models are prone to subtle programming errors, leading to development of multiple correctness checking tools. However, these are often limited to C/C++ codes, tied to specific library implementations, or restricted to certain error classes. Building on our prior work with CoVer, a generic, contract-based verification framework for parallel programming models, we extend CoVer's applicability to Fortran, enabling static and dynamic analysis across multiple programming languages. We adapted language-specific contract definitions and modified the analyses to support both C/C++ and Fortran programs. Our evaluation demonstrates that the enhanced version preserves CoVer's analysis accuracy and even revealed a bug in the MPI-BugBench testing framework, underscoring the effectiveness of the approach. The Fortran port of CoVer turns out to be substantially more efficient than the state-of-the-art tool MUST, while maintaining generality across languages. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_20410 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Extending Contract Verification for Parallel Programming Models to Fortran Oraji, Yussur Mustafa Bischof, Christian Distributed, Parallel, and Cluster Computing Programming Languages High-performance computing often relies on parallel programming models such as MPI for distributed-memory systems. While powerful, these models are prone to subtle programming errors, leading to development of multiple correctness checking tools. However, these are often limited to C/C++ codes, tied to specific library implementations, or restricted to certain error classes. Building on our prior work with CoVer, a generic, contract-based verification framework for parallel programming models, we extend CoVer's applicability to Fortran, enabling static and dynamic analysis across multiple programming languages. We adapted language-specific contract definitions and modified the analyses to support both C/C++ and Fortran programs. Our evaluation demonstrates that the enhanced version preserves CoVer's analysis accuracy and even revealed a bug in the MPI-BugBench testing framework, underscoring the effectiveness of the approach. The Fortran port of CoVer turns out to be substantially more efficient than the state-of-the-art tool MUST, while maintaining generality across languages. |
| title | Extending Contract Verification for Parallel Programming Models to Fortran |
| topic | Distributed, Parallel, and Cluster Computing Programming Languages |
| url | https://arxiv.org/abs/2604.20410 |