LART: Compiled Abstract Execution (Competition Contribution)

LART - LLVM abstraction and refinement tool - originates from the DIVINE model-checker [5,7], in which it was employed as an abstraction toolchain for the LLVM interpreter. In this contribution, we present a stand-alone tool that does not need a verification backend but performs the verification natively. The core idea is to instrument abstract semantics directly into the program and compile it into a native binary that performs program analysis. This approach provides a performance gain of native execution over the interpreted analysis and allows compiler optimizations to be employed on abstracted code, further extending the analysis efficiency. Compilation-based abstraction introduces new challenges solved by LART, like domain interaction of concrete and abstract values simulation of nondeterministic runtime or constraint propagation.