ICSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
Mon 15 Apr 2024 11:22 - 11:44 at Maria Helena Vieira da Silva - State Merging & Posters Chair(s): Alessandro Orso

We address the problem of constraint encoding explosion which hinders the applicability of state merging in symbolic execution. Specifically, our goal is to reduce the number of disjunctions and if-then-else expressions introduced during state merging. The main idea is to dynamically partition the symbolic states into merging groups according to a similar uniform structure detected in their path constraints, which allows to efficiently encode the merged path constraint and memory using quantifiers. To address the added complexity of solving quantified constraints, we propose a specialized solving procedure that reduces the solving time in many cases. Our evaluation shows that our approach can lead to significant performance gains.

Mon 15 Apr

Displayed time zone: Lisbon change

11:00 - 12:30
State Merging & PostersKLEE at Maria Helena Vieira da Silva
Chair(s): Alessandro Orso Georgia Institute of Technology
11:00
22m
Talk
State Merging for Concolic Testing of Event-driven Applications
KLEE
P: Maarten Vandercammen , Coen De Roover Vrije Universiteit Brussel
11:22
22m
Talk
State Merging with Quantifiers in Symbolic Execution
KLEE
P: David Trabish Tel Aviv University, Noam Rinetzky Tel Aviv University, Sharon Shoham Tel Aviv University, Vaibhav Sharma Amazon
DOI
11:50
5m
Poster
FastKLEE: Faster Symbolic Execution via Reducing Redundant Bound Checking of Type-safe Pointers
KLEE
P: Haoxin Tu Singapore Management University, Singapore, Lingxiao Jiang Singapore Management University, Xuhua Ding Singapore Management University, He Jiang Dalian University of Technology
11:55
5m
Poster
Input Grammar Oriented Symbolic Execution
KLEE
Ke Ma , Yunlai Luo National University of Defense Technology, P: Weijiang Hong National University of Defense Technology, Changsha, China, Zhenbang Chen School of Computer, National University of Defense Technology, China, Yufeng Zhang Hunan University, Ji Wang School of Computer, National University of Defense Technology, China
12:00
5m
Poster
Mixed Fixed-point and Floating-point Symbolic Execution
KLEE
P: Thom Hughes Imperial College London, Daniel Schemmel Imperial College London, Martin Nowack Imperial College London, Cristian Cadar Imperial College London
12:05
5m
Poster
SC-MCC Test Case Generation using Dynamic Symbolic Execution Engines
KLEE
Golla Monika Rani , P: Sangharatna Godboley National Institute of Technology Warangal, Joxan Jaffar National University of Singapore, Rasool Maghareh Huawei
12:10
5m
Poster
Towards Complete Fuzzing with KLEE
KLEE
Kanika Gupta National Institute of Technology, Warangal, P: Sangharatna Godboley National Institute of Technology Warangal
12:15
5m
Poster
TracerX - Pruning Dynamic Symbolic Execution with Weakest Precondition Interpolation
KLEE
P: Arpita Dutta National University of Singapore, Rasool Maghareh Huawei, Joxan Jaffar National University of Singapore
12:20
5m
Poster
Exploring Complexity Estimation with Symbolic Execution and Large Language Models
KLEE
Adrians Skapars University of Manchester, Youcheng Sun The University of Manchester, Yannic Noller Singapore University of Technology and Design, P: Corina S. Păsăreanu