LART: Compiled Abstract Execution (Competition Contribution)
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F22%3A00125302" target="_blank" >RIV/00216224:14330/22:00125302 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-030-99527-0_31" target="_blank" >http://dx.doi.org/10.1007/978-3-030-99527-0_31</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-99527-0_31" target="_blank" >10.1007/978-3-030-99527-0_31</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
LART: Compiled Abstract Execution (Competition Contribution)
Popis výsledku v původním jazyce
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ázev v anglickém jazyce
LART: Compiled Abstract Execution (Competition Contribution)
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10200 - Computer and information sciences
Návaznosti výsledku
Projekt
—
Návaznosti
S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2022
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems
ISBN
9783030995263
ISSN
0302-9743
e-ISSN
1611-3349
Počet stran výsledku
5
Strana od-do
457-461
Název nakladatele
Springer International Publishing
Místo vydání
Cham
Místo konání akce
Cham
Datum konání akce
1. 1. 2022
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
000782398900031