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

Symbolic execution (SE) is a widely used program analysis tech- nique. Existing SE engines model the memory space by associating memory objects with concrete addresses, where the representation of each allocated object is determined during its allocation. We present a novel addressing model where the underlying representa- tion of an allocated object can be dynamically modified even after its allocation, by using symbolic addresses rather than concrete ones. We demonstrate the benefits of our model in two applica- tion scenarios: dynamic inter- and intra-object partitioning. In the former, we show how the recently proposed segmented memory model can be improved by dynamically merging several object representations into a single one, rather than doing that a-priori using static pointer analysis. In the latter, we show how the cost of solving array theory constraints can be reduced by splitting the representations of large objects into multiple smaller ones. Our pre- liminary results show that our approach can significantly improve the overall effectiveness of the symbolic exploration.

Mon 20 Jul

Displayed time zone: Tijuana, Baja California change

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

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

12:10
20m
Talk
Fast Bit-Vector Satisfiability
Technical Papers
Peisen Yao HKUST, Qingkai Shi The Hong Kong University of Science and Technology, Heqing Huang , Charles Zhang The Hong Kong University of Science and Technology
DOI
12:30
20m
Talk
Relocatable Addressing Model for Symbolic Execution
Technical Papers
David Trabish Tel Aviv University, Noam Rinetzky Tel Aviv University
DOI Pre-print Media Attached
12:50
20m
Talk
Running Symbolic Execution ForeverArtifacts Evaluated – ReusableArtifacts AvailableArtifacts Evaluated – Functional
Technical Papers
Frank Busse Imperial College London, Martin Nowack Imperial College London, Cristian Cadar Imperial College London
DOI Pre-print Media Attached