Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on the NASA Java Pathfinder (JPF) model checker, which is used in research and industry labs. It executes Java bytecode using a custom JVM to perform its analysis.
It currently uses lazy initialization, a brute-force enumeration of all heap objects that can bind to the structured inputs accessed by the program. This explicit enumeration may lead to a huge amount of false alarms.
We propose to explore alternative ways of representing constraints over the heap. This would allow SPF to avoid a complete enumeration of all the possible cases, eliminating the ones violating the data structures properties. We want to focus in particular on separation logic and see if it brings an improvement compared to the lazy initialization or to languages like .