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

University Of Utah, Salt Lake City UT

Investigators

Abstract

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.