Symbolic Execution Without Execution: AI-Powered Constraint Prediction

Rong Feng, Vanisha Gupta, Viroopaksh Ernampati and Vivek Patel

Symbolic execution helps check programs by exploring different paths based on symbolic inputs. Tools like KLEE are commonly used because they can automatically detect bugs and create test cases. In this project, we wanted to see if a large language model like GPT 4o could simulate the kinds of outputs that KLEE generates. The idea was to explore whether LLMs could one day replace parts of symbolic execution to save time and resources. One specific goal was to have GPT-4o identify the most constrained path in a program—this is the execution path with the most symbolic conditions. These paths are especially important because they often represent edge cases that are harder to test and more likely to contain deep bugs. However, figuring this out usually requires fully running KLEE, which can be expensive. So, we tested whether GPT-4o could predict the KLEE outputs and the most complex path using a dataset of 100 C programs. Our results showed about 20% accuracy in generating KLEE-like outputs and identifying the most constrained path. While not highly accurate, this early work helps show what current LLMs can and can’t do when it comes to simulating symbolic execution.

Major: 
Computer Science
Exhibition Category: 
Engineering
Exhibition Format: 
Poster Presentation
Campus: 
University Park
Faculty Sponsor: 
Suman Saha
Poster Number: 
134