CS2: Modular Verification of Scientific Software using Model Checking, Symbolic Execution, and Abstraction

About This Grant

Software plays an increasingly important role in scientific discovery and innovation. Nuclear fusion, quantum science, space exploration, cancer research, and biotechnology are just a few of the many scientific disciplines benefitting from software. However, like all software, programs used in science may contain defects ("bugs") --- errors in the code or mistaken assumptions ---that can render the output erroneous. Consequently, developers of scientific software expend significant effort debugging their code, reducing their productivity. Worse, some defects evade even the most extensive debugging efforts. This project is developing tools to help developers easily find subtle defects in their code and even verify (under reasonable assumptions) that the code is defect-free. The project's novelties are: a new modular approach to the specification of program components based on simple mathematical abstractions that are familiar to scientists; simple-to-use, automated methods to verify a program component adheres to its specification (or report a defect when it does not); and the application of these techniques to two state-of-the-art scientific software packages. The project's impacts are, first, the advancement of software verification technology generally, which can reduce development costs and increase software quality throughout industry, government laboratories, and academia. Second, improving public confidence in the soundness of conclusions based on scientific software. Third, the training of students and scientists in the use of advanced verification techniques, contributing to a cultural change in the way scientific software is constructed. These advances are based on new symbolic execution techniques implemented in the CIVL model checker. Libraries are being developed to support abstract mathematical concepts such as "vector" and "matrix". Symbolic "representation functions" are used to tie these abstractions to the significantly more complex data structures in a scientific program. Such a function consumes a data structure (which may be distributed across multiple processes) in the program and returns the abstract construct represented by that structure. This allows the user to specify correctness properties on the abstract level while the model checker verifies that the program structures implement the abstract operations correctly. Model checking techniques are used to verify concurrent algorithms, such as those expressed using Message Passing Interface (MPI), OpenMP, or Compute Unified Device Architecture (CUDA). These techniques are being applied to select components of PETSc, a widely used numerical linear algebra library and core component of numerous software projects, and to Flash-X, a state-of-the-art multiphysics simulation system used in astrophysics and other scientific disciplines. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.