LART: Compiled Abstract Execution (Competition Contribution)

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

LAUKO Henrich ROČKAI Petr

Year of publication 2022
Type Article in Proceedings
Conference TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-030-99527-0_31
Keywords abstraction;abstract interpretation;abstract execution;compilation;compilation-based abstraction;LLVM;LART;formal verification;symbolic execution
Description LART – LLVM Abstraction & Refinement Tool – originates from the divine model-checker, 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.