IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2022 > LISSA: Lazy Initialization with Specialized Solver Aid

Juan Manuel Copia

Tuesday, September 27, 2022

11:00am Meeting room 302 & Zoom3 (pass: @s3)

Juan Manuel Copia, PhD Student, IMDEA Software Institute

LISSA: Lazy Initialization with Specialized Solver Aid


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.