JEDI: These aren't the JSON documents you're looking for...
Hütter, T.; Augsten, N.; Kirsch, C.; Carey, M.J.; Li, C.
SIGMOD '22: Proceedings of the 2022 International Conference on Management of Data. New York: Association for Computing Machinery, 2022. p. 1584-1597. ISSN 0730-8078. ISBN 978-1-4503-9249-5.
Stať ve sborníku
ASE: A Value Set Decision Procedure for Symbolic Execution
Abyaneh, A.S.; Kirsch, C.
Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering. IEEE Press, 2021. p. 203-214. ISBN 978-1-6654-0337-5.
Stať ve sborníku
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.
What we eval in the shadows: A large-scale study of eval in R programs