Towards Richer Challenge Problems for Scientific Computing Correctness

TL;DR

This work argues for specialized correctness challenge problems in scientific computing to bridge formal methods and the SC community, outlining Dimensions of Correctness and Pitfalls to guide design. It proposes a comprehensive, multi-layered framework (from numerics to domain-modeling, PDEs, and concurrency) for evaluating correctness in realistic SC applications, alongside guidelines to avoid over-specialization, toy problems, and misalignment with domain needs, including uncertainty and validation considerations. By promoting cross-disciplinary dialogue and realistic criteria, the paper aims to drive the development of verification techniques that address the rich, practical correctness challenges inherent in scientific computing across scales. This has potential to improve the reliability of SC software and better align verification methodologies with the needs of end-user scientists and HPC practitioners.

Abstract

Correctness in scientific computing (SC) is gaining increasing attention in the formal methods (FM) and programming languages (PL) community. Existing PL/FM verification techniques struggle with the complexities of realistic SC applications. Part of the problem is a lack of a common understanding between the SC and PL/FM communities of machine-verifiable correctness challenges and dimensions of correctness in SC applications. To address this gap, we call for specialized challenge problems to inform the development and evaluation of FM/PL verification techniques for correctness in SC. These specialized challenges are intended to augment existing problems studied by FM/PL researchers for general programs to ensure the needs of SC applications can be met. We propose several dimensions of correctness relevant to scientific computing, and discuss some guidelines and criteria for designing challenge problems to evaluate correctness in scientific computing.