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.