2022
LART: Compiled Abstract Execution (Competition Contribution)
LAUKO, Henrich a Petr ROČKAIZákladní údaje
Originální název
LART: Compiled Abstract Execution (Competition Contribution)
Autoři
LAUKO, Henrich (703 Slovensko, domácí) a Petr ROČKAI (703 Slovensko, garant, domácí)
Vydání
Cham, TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems, od s. 457-461, 5 s. 2022
Nakladatel
Springer International Publishing
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10200 1.2 Computer and information sciences
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
tištěná verze "print"
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/22:00125302
Organizační jednotka
Fakulta informatiky
ISBN
978-3-030-99526-3
ISSN
UT WoS
000782398900031
Klíčová slova anglicky
abstraction;abstract interpretation;abstract execution;compilation;compilation-based abstraction;LLVM;LART;formal verification;symbolic execution
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 6. 4. 2023 08:35, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
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.
Návaznosti
MUNI/A/1145/2021, interní kód MU |
|