Write a Blog >>
ASE 2021
Sun 14 - Sat 20 November 2021 Australia
Tue 16 Nov 2021 19:40 - 20:00 at Koala - Using Knowledge Chair(s): Dalal Alrajeh

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 so-called strided value intervals (SVI) 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 abstractions do not work, the overhead for trying still remains low.

Tue 16 Nov

Displayed time zone: Hobart change

19:00 - 20:00
Using KnowledgeResearch Papers at Koala
Chair(s): Dalal Alrajeh Imperial College London
Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and CostACM Distinguished Paper
Research Papers
Malte Mues TU Dortmund University, Falk Howar TU Dortmund University
Reducing Bug Triaging Confusion by Learning from Mistakes with a Bug Tossing Knowledge GraphACM Distinguished Paper
Research Papers
Yanqi Su Australian National University, Zhenchang Xing Australian National University, Xin Peng Fudan University, Xin Xia Huawei Software Engineering Application Technology Lab, Chong Wang Fudan University, Xiwei (Sherry) Xu CSIRO’s Data61, Liming Zhu CSIRO’s Data61; UNSW
ASE: A Value Set Decision Procedure for Symbolic Execution
Research Papers
Alireza S. Abyaneh University of Salzburg, Christoph Kirsch University of Salzburg; Czech Technical University