LART: Compiled Abstract Execution (Competition Contribution)
| Authors | |
|---|---|
| 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 | |
| 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: |