This project involves development of new software verification technologies focused on the numerical and mathematical aspects of scientific software. The aim is to facilitate the migration of scientific software from sequential or bulk-synchronous execution on homogeneous architectures to nondeterministic, asynchronous execution on complex, hierarchical, and heterogeneous architectures.

To verify correctness, we will use static analysis techniques based on formal verification, supplemented with dynamic analysis informed by numerical noise estimates. We will follow the design-by-contract philosophy of exploiting program modularity and library interfaces in establishing correctness. We will address applications within DOE, using the languages that are common within DOE (C/C++, Fortran) combined with multiple parallel programming paradigms (MPI, OpenMP, CUDA, etc.).

We will define how DOE applications can use contracts as a way to specify expected program behavior for the application code and underlying numerical algorithms. We will define the technology to generate verification conditions specific to DOE HPC applications and use both static analysis tools to verify many of these conditions and dynamic analysis to verify the remaining verification conditions and contracts.

Where a trusted implementation exists, correctness of a new, possibly more complex, implementation can be established through proof of equivalence of both implementations. We will develop new notions of ​“equivalence” for scientific programs based on the expected behavior of floating-point computations.