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

科学和高性能计算软件处理对科学，工程和社会更普遍的根本重要性问题。 例子包括应用程序来预测地震破坏，模拟全球气候，执行化学和生物系统的原子级模拟，并调查物质的电子结构。 这些节目为深刻的科学结论和对社会至关重要的决定提供信息。 由于这些原因，迫切需要开发有效的方法来调试和验证科学程序。 该项目提高了并发中间验证语言（CIVL）的可用性，性能和鲁棒性，CIVL是一种基于符号执行和模型检查的科学程序验证工具。 该项目的新颖之处在于（1）扩展了验证使用各种并行编程应用程序编程接口（API）的程序的能力，以及（2）验证程序的两个版本是等效的能力。 该项目的影响体现在使用CIVL帮助调试代码的软件开发人员的生产力提高，以及对最终软件正确性的信心增加。该项目沿着沿着三条路线改进CIVL：可用性，健壮性和语言覆盖率，以及性能。 可用性改进包括改进的错误报告和精确控制CIVL检查内容的能力。 通过纠正CIVL的数组模型中的限制，并增加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.