LART: Compiled Abstract Execution (Competition Contribution)

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

LAUKO Henrich ROČKAI Petr

Rok publikování 2022
Druh Článek ve sborníku
Konference TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-030-99527-0_31
Klíčová slova abstraction;abstract interpretation;abstract execution;compilation;compilation-based abstraction;LLVM;LART;formal verification;symbolic execution
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.