ASE: A Value Set Decision Procedure for Symbolic Execution
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F21%3A00365498" target="_blank" >RIV/68407700:21240/21:00365498 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1109/ASE51524.2021.9678584" target="_blank" >https://doi.org/10.1109/ASE51524.2021.9678584</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/ASE51524.2021.9678584" target="_blank" >10.1109/ASE51524.2021.9678584</a>
Alternative languages
Result language
angličtina
Original language name
ASE: A Value Set Decision Procedure for Symbolic Execution
Original language description
A symbolic execution engine regularly queries a Satisfiability Modulo Theory (SMT) solver to determine reachability of code during execution. Unfortunately, the SMT solver is often the bottleneck of symbolic execution. Inspired by abstract interpretation, we propose an abstract symbolic execution (ASE) engine which aims at querying the SMT solver less often by trying to compute reachability faster through an increasingly weaker abstraction. For this purpose, we have designed and implemented a value set decision procedure based on strided value interval (SVI) sets for efficiently determining precise, or under-approximating value sets for variables. Our ASE engine begins reasoning with respect to the SVI abstraction, and then only if needed uses the theory of bit-vectors implemented in SMT solvers. Our ASE engine efficiently detects when the former abstraction becomes incomplete to move on and try the next abstraction. We have designed and implemented a prototype of our engine for a subset of 64-bit RISC-V. Our experimental evaluation shows that our prototype often improves symbolic execution time by significantly reducing the number of SMT queries while, whenever the abstraction does not work, the overhead for trying still remains low.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/EF15_003%2F0000421" target="_blank" >EF15_003/0000421: Big Code: Scalable Analysis of Massive Code Bases</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering
ISBN
978-1-6654-0337-5
ISSN
—
e-ISSN
—
Number of pages
12
Pages from-to
203-214
Publisher name
IEEE Press
Place of publication
—
Event location
Melbourne
Event date
Nov 15, 2021
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000779309000020