CAREER: Ensuring the Accuracy of Scientific Software: A Formal Approach

University Of Delaware, Newark DE

Investigators

Abstract

Scientific practice has been radically transformed by computation. Many observers now place computational simulation on an equal footing with the two traditional approaches to scientific discovery, experimentation and theory. But while there are long-established and rigorous criteria for validating experiments and mathematical reasoning, the same is not true for simulation. Published reports of simulation-based research typically say little or nothing about the software, its qualities, or what was done to ascertain its correctness. The software is rarely examined by reviewers or other researchers, and in some cases is not even made available to them. This situation is particularly troublesome in light of the substantial evidence that scientific software is, in general, as unreliable as any other type of software. The research focuses on developing a set of integrated techniques for the specification and verification of scientific software. Drawing on ideas from model checking, symbolic execution, and other formal methods, these will include: (1) new techniques to efficiently check for the presence of deadlocks, race conditions, improper use of parallel programming libraries, and other generic defects in scientific programs, (2) techniques to specify and verify the order of accuracy of numerical programs, such as those used to solve systems of differential equations, and (3) new techniques to verify the functional equivalence of two scientific programs, including programs with unbounded loops, and programs with (shared-variable and/or message-passing) parallelism. These techniques will be realized in a new tool suite, the Toolkit for Accurate Scientific Software (TASS), which will be made publicly available under an open source license.