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.
@article{arxiv.2604.20410,
title = {Extending Contract Verification for Parallel Programming Models to Fortran},
author = {Yussur Mustafa Oraji and Christian Bischof},
journal= {arXiv preprint arXiv:2604.20410},
year = {2026}
}
Comments
A peer-reviewed version is to be published by Springer as part of the ISC C3PO workshop proceedings. This is the originally submitted article