SMACK: Decoupling Source Language Details from Verifier Implementations

Share

Zvonimir Rakamaric, Michael Emmi. 26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria.
[pdf] [bib]

Abstract: A major obstacle to putting software verification research into practice is the high cost of developing the infrastructure enabling the application of verification algorithms to actual production code, in all of its complexity. Handling an entire programming language is a huge endeavor that few researchers are willing to undertake; even fewer could invest the effort to implement a verification algorithm for many source languages. To decouple the implementations of verification algorithms from the details of source languages, and enable rapid prototyping on production code, we have developed SMACK. At its core, SMACK is a translator from the LLVM intermediate representation (IR) into the Boogie intermediate verification language (IVL). Sourcing LLVM exploits an increasing number of compiler front ends, optimizations, and analyses. Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation. Our initial experience in verifying C-language programs is encouraging: SMACK is competitive in SV-COMP benchmarks, is able to translate large programs (100 KLOC), and is being used in several verification research prototypes.

Experiments: To make our results readily reproducible, we created a virtual machine profile in the Apt testbed facility containing all used tools, scripts, and benchmarks. It is available at https://www.aptlab.net/p/fmr/smack-cav2014.

Bibtex:

@inproceedings{cav2014-re,
  author = {Zvonimir Rakamari\'c and Michael Emmi},
  title = {{SMACK}: Decoupling Source Language Details from Verifier Implementations},
  booktitle = {Proceedings of the 26th International Conference on Computer Aided
    Verification (CAV)},
  series = {Lecture Notes in Computer Science},
  volume = {8559},
  publisher = {Springer},
  editor = {Armin Biere and Roderick Bloem},
  year = {2014},
  pages = {106--113},
}