LART: Compiled Abstract Execution - (Competition Contribution)

Abstract

Abstract 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.