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.

翻译：高性能计算通常依赖于面向分布式内存系统的并行编程模型，例如MPI。这些模型功能强大，但容易出现细微的编程错误，因此推动了多种正确性检查工具的开发。然而，这些工具通常局限于C/C++代码、绑定特定库实现，或仅适用于某些错误类别。基于我们先前在CoVer上的工作——一个通用的、基于契约的并行编程模型验证框架，我们将CoVer的适用性扩展到Fortran，实现了跨多种编程语言的静态与动态分析。我们调整了语言特定的契约定义，并修改了分析过程以支持C/C++和Fortran程序。我们的评估表明，增强后的版本保持了CoVer的分析精度，甚至揭示了MPI-BugBench测试框架中的一个错误，凸显了该方法的有效性。Fortran版的CoVer在保持跨语言通用性的同时，其效率显著优于当前最先进的工具MUST。