Symbolic PathFinder (SPF) has been very successful in testing and verifying Java bytecode programs with numeric inputs. However, its capability is very limited when coping with programs that have heap data structures. The underlying lazy initialization algorithm exhaustively enumerates all heap objects that can bind to the structured inputs accessed by the program. This enumeration may identify many invalid heap configurations that violate properties of the data structures in the heap, which leads to a huge amount of false alarms.
We aim to tackle this problem by using separation logic, a well-known assertion language designed for reasoning about heap-manipulating programs. We will build a system, Java StarFinder (JSF), that enables users to describe properties of the data structures in the heap using separation logic. JSF is a symbolic execution engine, built on top of SPF, that generates path conditions (PCs) in the form of separation logic. These PCs are checked by a solver for satisfiability and test input generation. In addition, JSF can verify program correctness by collecting PCs satisfying some given preconditions and verifying if these PCs satisfy user-provided assertions.