Finding bugs is hard, sometimes impossible, and tends to take long. One popular and successful automated technique is the dynamic execution of code with some variables treated as symbolic. This approach is known as Symbolic Execution. Symbolic Execution takes every branch of the program, and applies appropriate constraints to the symbols to represent all concrete values that would reach that particular branch. Until recently, this technique has not been able to deal with strings. We present a new approach to Symbolic Execution with strings, implemented in Java Pathfinder by means of finite automata and bit-vectors (via SMT Solvers), and it is capable of executing over symbolic strings and (a first) over symbolic integers that are dependent on symbolic strings. We shall give a demonstration of how the tool finds an error in string handling code that caused an infinite loop in a production setting; to the best of our knowledge, no other tool is capable of finding this error.
Gideon Redelinghuys is a masters student at Computer Science, Stellenbosch.