Další formáty:
BibTeX
LaTeX
RIS
@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.
|
