Abstract
Tool prototyping is an essential step in developing novel software verification algorithms and techniques. However, implementing a verifier prototype that can handle real-world programs is a huge endeavor, which hinders researchers by forcing them to spend more time engineering tools, and less time innovating. In this paper, we present the SMACK software verification toolchain. The toolchain provides a modular and extensible software verification ecosystem that decouples the front-end source language details from back-end verification algorithms. It achieves that by translating from the LLVM compiler intermediate representation into the Boogie intermediate verification language. SMACK benefits the software verification community in several ways: (i) it can be used as an off-the-shelf software verifier in an applied software verification project, (ii) it enables researchers to rapidly develop and release new verification algorithms, (iii) it allows for adding support for new languages in its front-end. We have used SMACK to verify numerous C/C++ programs, including industry examples, showing it is mature and competitive. Likewise, SMACK is already being used in several existing verification research prototypes.
Citation
Montgomery Carter,
Shaobo He,
Jonathan Whitaker,
Zvonimir Rakamaric,
Michael Emmi
SMACK Software Verification Toolchain
Proceedings of the 38th IEEE/ACM International Conference on Software Engineering (ICSE) Companion, 589--592, doi:10.1145/2889160.2889163, 2016.
BibTeX
@inproceedings{2016_icse_chwre,
title = {SMACK Software Verification Toolchain},
author = {Montgomery Carter and Shaobo He and Jonathan Whitaker and Zvonimir Rakamaric and Michael Emmi},
booktitle = {Proceedings of the 38th IEEE/ACM International Conference on Software Engineering (ICSE) Companion},
publisher = {ACM},
editor = {Willem Visser and Laurie Williams},
pages = {589--592},
doi = {10.1145/2889160.2889163},
year = {2016}
}
Acknowledgements
Supported in part by the University of Utah Office of Undergraduate Research and NSF CCF 1346756/1421678.