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

科学实践已经被计算彻底改变了。许多观察家现在把计算模拟与科学发现的两种传统方法——实验和理论——放在同等的地位上。但是，虽然在验证实验和数学推理方面有长期建立的严格标准，但在模拟方面却并非如此。发表的基于模拟的研究报告通常很少或根本没有提到软件，它的质量，或者做了什么来确定它的正确性。这些软件很少被审稿人或其他研究人员检查，在某些情况下甚至不提供给他们。这种情况尤其麻烦，因为有大量证据表明，科学软件通常和其他类型的软件一样不可靠。研究的重点是开发一套科学软件规范与验证的集成技术。从模型检查、符号执行和其他形式化方法中汲取灵感，这些方法包括：(1)有效检查死锁、竞争条件、并行编程库使用不当和科学程序中其他一般缺陷的新技术；(2)指定和验证数值程序（如用于求解微分方程组的程序）的精度顺序的技术；(3)验证两个科学程序（包括具有无界循环的程序）的功能等价的新技术；具有（共享变量和/或消息传递）并行性的程序。这些技术将在新的工具套件中实现，即精确科学软件工具包（TASS），它将在开放源代码许可下公开提供。

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.