ICSE 2024 (series) / KLEE 2024 (series) / KLEE 2024 /
State Merging with Quantifiers in Symbolic Execution
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 AprDisplayed time zone: Lisbon change
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 22mTalk | State Merging for Concolic Testing of Event-driven Applications KLEE | ||
11:22 22mTalk | 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 5mPoster | 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 5mPoster | 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 5mPoster | 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 5mPoster | 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 5mPoster | Towards Complete Fuzzing with KLEE KLEE Kanika Gupta National Institute of Technology, Warangal, P: Sangharatna Godboley National Institute of Technology Warangal | ||
12:15 5mPoster | 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 5mPoster | 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 |