IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series > 2022 > LISSA: Lazy Initialization with Specialized Solver Aid
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Juan Manuel Copia

martes 27 de septiembre de 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.