FMitF: Track II: Lifting the SMACK Verifier to Production Software

如今软件无处不在。 软件系统运行的设备从心脏起搏器、电话和计算机，一直到卡车、飞机和智能电网。这些系统非常复杂，很难正确实现，其中的错误可能会产生非常严重的后果。因此，开发人员需要现成的工具来帮助他们确保软件系统的正确性。该项目旨在改进和扩展一个这样的工具，称为SMACK，并使其能够作为常规软件开发实践的一部分，以帮助开发人员创建更好的软件。SMACK被学术界的研究人员和行业从业者使用。研究人员使用它，因为它可以轻松地实验新的验证算法和技术。从业者使用它，因为它是一个稳定的软件验证器，适用于中小型软件系统。拟议的功能和补充将进一步提高SMACK的能力，以推动新的软件验证研究和软件验证在行业实践中的采用。该项目还将通过制作大量基准测试来提高软件验证研究的可重复性，并通过开发教学模块和教程来促进软件验证教育。该项目分为三个主要任务：支持更多的源语言功能，验证大型软件系统，以及实现可调的可扩展性和验证精度。支持现代源语言功能，如特殊的并行性和安全相关的指令，需要为它们发明适合验证的模型。大型软件系统导致了新的验证算法和实现的开发，例如利用当今机器中可用的大规模并行性的算法和实现。 最后，具有可调整的可扩展性和精度需要在这个空间中的各种选项的经验探索，这进一步了解哪些验证技术在现实世界的软件系统上工作。该项目的目标是建立一个行业实力的软件验证器，跟上验证技术和软件实践的发展。因此，SMACK的大致寿命预计将远远超出本项目的范围，达到10-15年。SMACK作为GitHub（https：//github.com/smackers/smack）上的许可开源项目已经有八年的时间了，它还利用了流行的开源项目，如低级虚拟机（LLVM）编译器基础设施。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Software is ubiquitous nowadays. Software systems run devices ranging from pacemakers, phones, and computers, all the way to trucks, airplanes, and smart power grids. These systems are extremely complex and hard to implement correctly, and errors in them can have very serious consequences. Therefore, developers need readily available tools to help them ensure the correctness of software systems. This project aims to improve and extend one such tool, called SMACK, and enable for it to be used as a part of the regular software-development practice to help developers create better software.SMACK is used both by researchers in academia and industry practitioners. Researchers use it since it enables easy experimentation with new verification algorithms and techniques. Practitioners use it since it is a stable software verifier that works on small- to medium-sized software systems. The proposed features and additions will further increase SMACK's capabilities to drive novel software-verification research and the adoption of software verification in industry practice. The project will also increase the reproducibility of software-verification research by producing a large number of benchmarks, and promote software-verification education through the development of teaching modules and tutorials.The project is split into three main tasks: supporting more source-language features, verifying large software systems, and enabling adjustable scalability and precision of verification. Supporting modern source-language features, such as special parallelism- and security-related instructions, requires inventing models for them that are appropriate for verification. Verifying large software systems leads to the development of novel verification algorithms and implementations, such as the ones that leverage massive parallelism available in machines nowadays. Finally, having adjustable scalability and precision requires empirical exploration of various options in this space, which furthers the understanding of which verification techniques work on real-world software systems.The goal of the project is to build an industry-strength software verifier that keeps up with the development of verification technology and software practices. Hence, the approximate lifetime of SMACK is expected to extend far beyond the scope of this project, into the range of 10-15 years. SMACK has been available as a permissively-licensed open-source project on GitHub (https://github.com/smackers/smack) for eight years already, and it also leverages popular open-source projects such as the low level virtual machine (LLVM) compiler infrastructure. The plan to ensure its longevity is to continue embracing the open-source community through public bug reports, development subtasks, and peer code reviews.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.