Conference Proceedings

State Joining and Splitting for the Symbolic Execution of Binaries

TA HANSEN, P SCHACHTE, H SONDERGAARD, S Bensalem (ed.), DA Peled (ed.)

Lecture Notes in Computer Science: Runtime Verification | Springer Berlin Heidelberg | Published : 2009


Symbolic execution can be used to explore the possible run-time states of a program. It makes use of a concept of "state" where a variable's value has been replaced by an expression that gives the value as a function of program input. Additionally, a state can be equipped with a summary of control-flow history: a "path constraint" keeps track of the class of inputs that would have caused the same flow of control. But even simple programs can have trillions of paths, so a path-by-path analysis is impractical. We investigate a "state joining" approach to making symbolic execution more practical and describe the challenges of applying state joining to the analysis of unmodified Linux x86 execut..

View full abstract