Bounded Lazy Initialization

JACO GELDENHUYS; AGUIRRE, NAZARENO; FRIAS, MARCELO FABIAN; VISSER, WILLEM

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Año: 2013 p. 229 - 243

0302-9743

Tight field bounds have been successfully used in the con- text of bounded-exhaustive bug finding. They allow us to check the cor- rectness of, or find bugs in, code manipulating data structures whose size made this kind of analyses previously infeasible. In this article we address the question of whether tight bounds can also contribute to a significant speed-up for symbolic execution when using a system such as Symbolic Pathfinder. Specifically, its lazy initialization algorithm was changed to take advantage of field bounds. While the straightforward approach to adding bounds works well for small bounds, the lack of symmetry-breaking significantly affects its performance. We introduce a new technique that generates only non-isomorphic structures and is therefore able to consider fewer structures and to execute faster than lazy initialization.