A technique for dealing with code that manipulates pointer data structures. As the name suggests, instead of constructing an input data structure first and then symbolically executing the code, the data structure is constructed on demand: each dereference of an uninitialized pointer either constructs a fresh object or chooses one of the previously constructed objects that the pointer could potentially refer to.
The original version (khurshid:tacas:2003) could handle shared data structures and cycles because it tracked previously initialized objects and allowed the pointer to refer to one of them or to a fresh object.
Later uses of the idea (e.g., xie:popl:2005, engler:issta:2007) always created a fresh object and so could not reason about shared/cyclic data structures.
Papers related to Lazy initialization of symbolic values
- Sys: A static/symbolic tool for finding good bugs in good (browser) code [brown:sec:2020]
- Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
- Under-constrained execution: Making automatic code destruction easy and scalable [engler:issta:2007]
- Micro execution [godefroid:icse:2014]
- Generalized symbolic execution for model checking and testing [khurshid:tacas:2003]
- Practical, low-effort equivalence verification of real code [ramos:cav:2011]
- Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]
- Scalable error detection using boolean satisfiability [xie:popl:2005]