FMitF: Track II: Usability, Robustness, and Performance Improvements for CIVL

FMITF：轨道 II：CIVL 的可用性、稳健性和性能改进

• 批准号: 2019309
• 负责人: Stephen Siegel
• 金额: $ 10万
• 依托单位: University of Delaware
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2023-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019309&HistoricalAwards=false
• 关键词: FMitF; Track; II; Usability; Robustness

Scientific and high-performance computing software deals with issues of fundamental importance to science, engineering, and society more generally. Examples include applications to predict earthquake damage, model the global climate, perform atomic-level simulations of chemical and biological systems, and to investigate the electronic structure of matter. These programs inform both profound scientific conclusions and decisions of the utmost importance to society. For these reasons, it is imperative to develop effective methods for debugging and verifying scientific programs. This project enhances the usability, performance, and robustness of the Concurrent Intermediate Verification Language (CIVL), a verification tool for scientific programs based on symbolic execution and model checking. The project's novelties are (1) an expanded ability to verify programs that use a variety of parallel-programming Application Programming Interfaces (APIs), and (2) the capability to verify that two versions of a program are equivalent. The project's impacts are seen in the improved productivity of the software developers using CIVL to help debug their code, and in the increased confidence in the correctness of the resulting software.The project improves CIVL along three lines: usability, robustness and language coverage, and performance. Usability improvements include improved error reporting and the ability to control precisely what CIVL checks. Language coverage is improved by correcting limitations in CIVL's array model, and increasing coverage of the C standard library. Performance is being improved by parallelizing CIVL's model-checking engine and streamlining its expression-evaluation algorithm. These improvements are guided by ongoing interaction with scientific-software development teams who are using CIVL and providing feedback.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.

科学和高性能计算软件更广泛地涉及对科学，工程和社会的根本重要性。 例子包括用于预测地震损害的应用，建模全球气候，进行化学和生物系统的原子水平模拟以及研究物质的电子结构。 这些计划既可以为社会最重要的深刻科学结论和决定。 由于这些原因，必须开发有效的方法来调试和验证科学计划。 该项目增强了并发中间验证语言（CIVL）的可用性，性能和鲁棒性，这是一种基于符号执行和模型检查的科学程序的验证工具。 项目的新颖性是（1）扩展的能力，可以验证使用各种并行编程的应用程序编程接口（API）的程序，以及（2）验证程序的两个版本是否等效的能力。 在使用CIVL来帮助调试代码的软件开发人员的生产率上，可以看到该项目的影响，并提高了对所得软件正确性的信心。该项目沿着三行：可用性，鲁棒性和语言覆盖范围和性能提高了CIVL。 可用性提高包括改进的错误报告以及精确控制CIVL检查的能力。 通过纠正CIVL阵列模型中的限制以及增加C标准库的覆盖范围，可以改善语言覆盖范围。 通过并行化CIVL的模型检查引擎并简化其表达评估算法，从而提高了性能。 这些改进是通过与使用CIVL并提供反馈的科学软件开发团队进行的持续互动来指导的。该奖项反映了NSF的法定使命，并使用基金会的知识分子优点和更广泛的影响审查标准，认为值得通过评估来获得支持。