LART: Compiled Abstract Execution (Competition Contribution)

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
LART: Compiled Abstract Execution (Competition Contribution)
Original language description
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.
Czech name
—
Czech description
—

Project
—
Continuities
S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems
ISBN
9783030995263
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
5
Pages from-to
457-461
Publisher name
Springer International Publishing
Place of publication
Cham
Event location
Cham
Event date
Jan 1, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000782398900031

Similar results(10)