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

点击翻译按钮获取中文摘要

Scientific practice has been radically transformed by computation.Many observers now place computational simulation on an equal footingwith the two traditional approaches to scientific discovery,experimentation and theory. But while there are long-established andrigorous criteria for validating experiments and mathematicalreasoning, the same is not true for simulation. Published reports ofsimulation-based research typically say little or nothing about thesoftware, its qualities, or what was done to ascertain itscorrectness. The software is rarely examined by reviewers or otherresearchers, and in some cases is not even made available to them.This situation is particularly troublesome in light of the substantialevidence that scientific software is, in general, as unreliable as anyother type of software.The research focuses on developing a set of integrated techniques forthe specification and verification of scientific software. Drawing onideas from model checking, symbolic execution, and other formalmethods, these will include: (1) new techniques to efficiently checkfor the presence of deadlocks, race conditions, improper use ofparallel programming libraries, and other generic defects inscientific programs, (2) techniques to specify and verify the order ofaccuracy of numerical programs, such as those used to solve systems ofdifferential equations, and (3) new techniques to verify thefunctional equivalence of two scientific programs, including programswith unbounded loops, and programs with (shared-variable and/ormessage-passing) parallelism. These techniques will be realized in anew tool suite, the Toolkit for Accurate Scientific Software (TASS),which will be made publicly available under an open source license.