SMACK: Decoupling source language details from verifier implementations

Zvonimir Rakamarić, Michael Emmi
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 08 October 2019

International Conference on Computer Aided Verification
Springer
Pages 106-113
2014
Topic(s): tools verification
Note(s): Boogie verifier, intermediate verification language, SMACK verifier, LLVM compiler

SMACK translates LLVM bitcode files to the Boogie language (an intermediate verification language) allowing it to support any language that LLVM supports (mostly C/C++ in this paper).

SMACK implements one key optimization: using alias analysis to partition the heap (and pointers into the heap) so that objects that could not be confused are in separate sub-heaps.

SMACK verifier