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

如今，软件无处不在。从起搏器、电话、电脑，一直到卡车、飞机和智能电网，软件系统都在运行。这些系统极其复杂，难以正确实现，其中的错误可能会产生非常严重的后果。因此，开发人员需要随时可用的工具来帮助他们确保软件系统的正确性。这个项目的目标是改进和扩展一个这样的工具，称为SMACK，并使它能够作为常规软件开发实践的一部分来使用，以帮助开发人员创建更好的软件。SMACK既被学术界的研究人员使用，也被行业从业者使用。研究人员使用它是因为它使新的验证算法和技术的实验变得容易。从业者使用它是因为它是一种稳定的软件验证器，可以在小型到中型软件系统上工作。提出的特性和附加功能将进一步提高SMACK的能力，以推动新颖的软件验证研究和在工业实践中采用软件验证。该项目还将通过生成大量基准来增加软件验证研究的可重复性，并通过开发教学模块和教程来促进软件验证教育。该项目分为三个主要任务：支持更多的源语言特性，验证大型软件系统，以及启用可调整的可伸缩性和验证的精度。支持现代源语言特性，例如特殊的并行性和安全性相关指令，需要为它们发明适合于验证的模型。验证大型软件系统会导致新的验证算法和实现的发展，例如利用当今机器中可用的大规模并行性的算法和实现。最后，具有可调节的可伸缩性和精度需要对该领域的各种选项进行经验探索，这将进一步了解哪些验证技术适用于真实的软件系统。该项目的目标是构建一个行业强度的软件验证器，以跟上验证技术和软件实践的发展。因此，SMACK的使用寿命预计将远远超出本项目的范围，达到10-15年的范围。SMACK已经在GitHub （https://github.com/smackers/smack）上作为许可许可的开源项目提供了8年，它还利用了流行的开源项目，如低级虚拟机（LLVM）编译器基础设施。确保其寿命的计划是通过公开bug报告、开发子任务和同行代码审查继续拥抱开源社区。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.