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

职业：确保科学软件的准确性：正式方法

• 批准号: 0953210
• 负责人: Stephen Siegel
• 金额: $ 41.17万
• 依托单位: University of Delaware
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-04-01 至 2016-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0953210&HistoricalAwards=false
• 关键词: CAREER; Ensuring; Accuracy; Scientific; Software

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.

科学实践已经通过计算从根本上改变了。许多观察者现在将计算模拟在同等的基础上放置在科学发现，实验和理论的两种传统方法上。 但是，尽管有悠久的良好标准用于验证实验和数学策划，但模拟并非如此。 发表的基于仿真的研究的报告通常很少或一无所知。 该软件很少受审阅者或其他研究人员的检查，在某些情况下甚至没有提供该软件。鉴于科学软件通常与其他任何类型的软件一样不可靠的证明，这种情况尤其令人麻烦。研究的重点是开发一系列集成技术来开发一系列用于科学软件的综合技术。 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）验证两个科学程序的功能等效性的新技术，包括程序间无限的循环以及具有（共享变量和/ormessage-passage）并行性的程序。 这些技术将在Enew Tool Suite（准确的科学软件（TASS））的Enew Tool Suite中实现，该工具包将根据开源许可证公开提供。