Dynamic symbolic execution (DSE) is an effective tool for bug detection in real software. Like unit testing and fuzzing DSE executes portions of a program, exposing bugs through runtime program exceptions. In DSE, some inputs to the program under test are made “symbolic” while the rest are fixed. Whenever the symbolic execution encounters a conditional operation depending on symbolic inputs, it uses a constraint solver to derive inputs that would drive down execution on either side. In principle, this allows to fully automatically generate test cases covering all possible paths in a program.
Some external functions are opaque to DSE, however, and it is unable to derive their effects on symbolic variables. To allow successful exploration of programs using external functions (which can involve standard library functions for input / output / string processing, etc.), one must declare equivalent models, which are simplified versions of the library functions focusing on possible return values and effects on arguments. Each additional model increases the effectiveness of DSE.