Testing heap-based programs with Java StarFinder

Long H. Pham, Quang Loc Le, Quoc Sang Phan, Jun Sun, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present Java StarFinder (JSF), a tool for automated test case generation and error detection for Java programs having inputs in the form of complex heap-manipulating data structures. The core of JSF is a symbolic execution engine that uses separation logic with existential quantifiers and inductively-defined predicates to precisely represent the (unbounded) symbolic heap. The feasibility of a heap configuration is checked by a satisfiability solver for separation logic. At the end of each feasible path, a concrete model of the symbolic heap (returned by the solver) is used to generate a test case, e.g., a linked list or an AVL tree, that exercises that path. We show the effectiveness of JSF by applying it on non-Trivial heap-manipulating programs and evaluated it against JBSE, a state-of-The-Art symbolic execution engine for heap-based programs. Experimental results show that our tool significantly reduces the number of invalid test inputs and improves the test coverage.

Original languageEnglish
Title of host publicationProceedings - International Conference on Software Engineering
PublisherIEEE Computer Society
Number of pages2
ISBN (Electronic)9781450356633
Publication statusPublished - 27 May 2018
Event40th ACM/IEEE International Conference on Software Engineering - Gothenburg, Sweden
Duration: 27 May 20183 Jun 2018


Conference40th ACM/IEEE International Conference on Software Engineering
Abbreviated titleICSE 2018


Dive into the research topics of 'Testing heap-based programs with Java StarFinder'. Together they form a unique fingerprint.

Cite this