ICST 2023
Sun 16 - Thu 20 April 2023 Dublin, Ireland

Symbolic execution (SE) is a popular program analysis technique. SE heavily relies on satisfiability queries during path exploration, often resulting in the majority of the time being spent on solving these queries. Hence, it is not surprising that one of the most vital optimizations SE engines use is query caching. To increase the cache hit rate, queries are transformed into a normal form, which is used as a key for updating the cache. An obstacle to caching queries involving pointers is the presence of numerical address values, which are assigned by the engine according to its memory allocation scheme and are hard to canonicalize across different paths.In this paper, we propose a novel query caching technique that allows efficient handling of queries containing expressions that depend on address values. The key insight is that the result of such queries is in fact agnostic to the concrete address values occurring in them, subject to some basic memory safety constraints. This observation can be used to coalesce more queries during cache lookup, thus further increasing cache utilization.Our extensive evaluation shows that our technique achieves significant performance gains when the analysis encounters queries containing symbolic pointers, while incurring only a modest performance overhead in other cases.

Wed 19 Apr

Displayed time zone: Dublin change

11:00 - 12:30
Session 13: Testing with Static Analysis MethodsResearch Papers / Previous Editions at Pearse suite
Chair(s): Paolo Arcaini National Institute of Informatics
11:00
20m
Talk
Address-Aware Query Caching for Symbolic Execution
Previous Editions
David Trabish Tel Aviv University, Shachar Itzhaky Technion, Noam Rinetzky Tel Aviv University
DOI
11:20
20m
Talk
Automating Differential Testing with Overapproximate Symbolic Execution
Previous Editions
Richard Rutledge Georgia Institute of Technology, Alessandro Orso Georgia Tech
DOI
11:40
20m
Talk
Two Sparsification Strategies for Accelerating Demand-Driven Pointer Analysis
Research Papers
Kadiray Karakaya Heinz Nixdorf Institut, Paderborn University, Eric Bodden
Pre-print Media Attached
12:00
20m
Talk
Model Generation For Java Frameworks
Research Papers
Linghui Luo Amazon Web Services, Goran Piskachev Amazon Web Services, Ranjith Krishnamurthy Fraunhofer IEM, Julian Dolby IBM Research, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM, Martin Schäf Amazon Web Services