In this artifact we provide (Java) implementations for the symbolic execution approach LISSA and the SymSolve solver for partially symbolic structures. The symbolic execution approach of LISSA is tailored to efficiently deal with programs manipulating heap-allocated inputs that impose complex structural constraints (preconditions) on the inputs, operationally captured via repOK (Java) methods. LISSA is implemented on top of the lazy initialization engine of Symbolic Java PathFinder.

LISSA is based on a novel solver, SymSolve, that automatically and efficiently decides whether partially symbolic structures produced by lazy initialization can be extended to fully concrete structures satisfying the precondition (repOK). LISSA employs SymSolve to identify spurious symbolic structures (those that cannot be extended to concrete structures) and prune their corresponding paths in the symbolic execution tree, significantly reducing the number of paths LISSA needs to explore, and making it faster than related approaches.

We also provide a replication package for the experiments in the ASE’22 paper introducing LISSA: “LISSA: Lazy Initialization with Specialized Solver Aid”. In the experiments, we assessed LISSA against related techniques over various case studies consisting of programs manipulating heap-allocated inputs with complex constraints, and observed that LISSA is faster and scales better than related techniques.