Write a Blog >>
ISSTA 2020
Sat 18 - Wed 22 July 2020
Mon 20 Jul 2020 12:10 - 12:30 at Zoom - SYMBOLIC EXECUTION AND CONSTRAINT SOLVING Chair(s): Marcelo d'Amorim

SMT solving is often a major source of cost in a broad range of techniques such as symbolic execution. Thus, speeding up SMT solving is still an urgent requirement. A dominant approach, which is known as eager SMT solving, is to reduce a first-order formula to a pure Boolean formula, which is handed to an expensive SAT solver to determine the satisfiability. We observe that the SAT solver can utilize the knowledge in the first-order formula to boost its solving efficiency. Unfortunately, despite much progress, it is still not clear how to make use of the knowledge in an eager SMT solver. This paper addresses the problem by introducing a new and fast method, which utilizes the interval and data-dependence information learned from the first-order formulas. We have implemented the approach as a tool called Trident and evaluated it on three symbolic analysis platforms (Angr, Qsym, and Pinpoint). The experimental results, based on thirty real-world projects that generate about seven million queries, show that our approach significantly reduces the total solving time from 2.9x to 7.9x over three state-of-the-art SMT solvers (Z3, CVC4, and Boolector), without sacrificing the number of solved instances. We also demonstrate that Trident achieves end-to-end speedups for three program analysis clients by 1.9x, 1.6x, and 2.4x, respectively.

Mon 20 Jul
Times are displayed in time zone: Tijuana, Baja California change

12:10 - 13:10: SYMBOLIC EXECUTION AND CONSTRAINT SOLVINGTechnical Papers at Zoom
Chair(s): Marcelo d'AmorimFederal University of Pernambuco

Public Live Stream/Recording. Registered participants should join via the Zoom link distributed in Slack.

12:10 - 12:30
Fast Bit-Vector Satisfiability
Technical Papers
Yao PeisenHKUST, Qingkai ShiThe Hong Kong University of Science and Technology, Heqing Huang, Charles ZhangThe Hong Kong University of Science and Technology
12:30 - 12:50
Relocatable Addressing Model for Symbolic Execution
Technical Papers
David TrabishTel Aviv University, Noam RinetzkyTel Aviv University
DOI Pre-print Media Attached
12:50 - 13:10
Running Symbolic Execution ForeverArtifacts Evaluated – ReusableArtifacts AvailableArtifacts Evaluated – Functional
Technical Papers
Frank BusseImperial College London, Martin NowackImperial College London, Cristian CadarImperial College London
DOI Pre-print Media Attached