SMACK Software Verification Toolchain

Share

Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, Michael Emmi. Demonstrations Track at the 38th IEEE/ACM International Conference on Software Engineering (ICSE 2016), Austin, TX, USA.
[pdf] [bib]

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. Our demonstration of SMACK can be found on YouTube at the following address: https://youtu.be/SPPSC1KdRzs

Bibtex:

@inproceedings{icse2016-chwre,
  author = {Montgomery Carter and Shaobo He and Jonathan Whitaker and
    Zvonimir Rakamari\'c and Michael Emmi},
  title = {{SMACK} Software Verification Toolchain},
  booktitle = {Proceedings of the 38th IEEE/ACM International
    Conference on Software Engineering (ICSE) Companion},
  publisher = {ACM},
  editor = {Willem Visser and Laurie Williams},
  year = {2016},
  pages = {589--592},
}