Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization (LI) is an approach to SE that deals with heap-allocated inputs by starting SE over a fully symbolic heap, and initializing the inputs’ fields on demand, as the program under analysis accesses them. However, when the program’s assumed precondition has structural constraints over the inputs, operationally captured via repOK routines, LI may produce spurious symbolic structures, making SE traverse infeasible paths and undermining SE’s performance.

In this talk I will present LISSA, our solution to efficiently detect and prune paths containing spurious symbolic structures. LISSA employs a novel structural constraint solver, SymSolve, capable of deciding satisfiability of partially symbolic structures. We experimentally assess LISSA against related techniques over various case studies, consisting of programs with heap-allocated inputs with complex constraints. The results show that LISSA is faster and scales better than related techniques.