LART: Compiled Abstract Execution (Competition Contribution)

D 2022

LART: Compiled Abstract Execution (Competition Contribution)

LAUKO, Henrich a Petr ROČKAI

Zá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

DOI

http://dx.doi.org/10.1007/978-3-030-99527-0_31

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

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. (Akronym: SV-FI MAV XI.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI.

Citovat

LAUKO, Henrich a Petr ROČKAI. LART: Compiled Abstract Execution (Competition Contribution). In Fisman, Dana and Rosu, Grigore. TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer International Publishing, 2022, s. 457-461. ISBN 978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0_31.

@inproceedings{1828538,
   author = {Lauko, Henrich and Ročkai, Petr},
   address = {Cham},
   booktitle = {TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems},
   doi = {http://dx.doi.org/10.1007/978-3-030-99527-0_31},
   editor = {Fisman, Dana and Rosu, Grigore},
   keywords = {abstraction;abstract interpretation;abstract execution;compilation;compilation-based abstraction;LLVM;LART;formal verification;symbolic execution},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-99526-3},
   pages = {457-461},
   publisher = {Springer International Publishing},
   title = {LART: Compiled Abstract Execution (Competition Contribution)},
   year = {2022}
}

TY  - JOUR
ID  - 1828538
AU  - Lauko, Henrich - Ročkai, Petr
PY  - 2022
TI  - LART: Compiled Abstract Execution (Competition Contribution)
PB  - Springer International Publishing
CY  - Cham
SN  - 9783030995263
KW  - abstraction;abstract interpretation;abstract execution;compilation;compilation-based abstraction;LLVM;LART;formal verification;symbolic execution
N2  - 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.
ER  -

LAUKO, Henrich a Petr ROČKAI. LART: Compiled Abstract Execution (Competition Contribution). In Fisman, Dana and Rosu, Grigore. \textit{TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems}. Cham: Springer International Publishing, 2022, s.~457-461. ISBN~978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0\_{}31.

Podrobný výpis o publikaci