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

科学和高性能计算软件处理对科学、工程和更广泛的社会具有根本重要性的问题。例子包括预测地震破坏、模拟全球气候、对化学和生物系统进行原子级模拟以及研究物质的电子结构等应用。这些项目既提供了深刻的科学结论，也提供了对社会至关重要的决定。出于这些原因，必须开发有效的方法来调试和验证科学程序。该项目增强了并发中间验证语言(CIVIL)的可用性、性能和健壮性，该语言是一种基于符号执行和模型检测的科学程序验证工具。该项目的创新之处在于(1)扩展了验证使用各种并行编程应用程序编程接口(API)的程序的能力，以及(2)验证程序的两个版本是否相等的能力。该项目的影响体现在软件开发人员使用CIVL来帮助调试他们的代码的生产率的提高，以及对结果软件正确性的信心的增加。该项目从三个方面改进了CIVL：可用性、健壮性、语言覆盖率和性能。易用性方面的改进包括改进了错误报告，并能够精确控制CIVIL检查的内容。语言的覆盖率通过修正Cistl数组模型中的限制和增加C标准库的覆盖率而得到提高。通过将CIVL的模型检查引擎并行化并简化其表达式求值算法，性能正在得到提高。这些改进是通过与使用CIVL并提供反馈的科学软件开发团队的持续互动来指导的。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.