Test input generation using separation logic
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
eclipse
expected-output
lib
nbproject
src
tools
.classpath
.gitignore
.project
Dockerfile
LICENSE
README.md
build.xml
jpf.properties

README.md

Java StarFinder

Java StarFinder (JSF) is a unit test generation tool for programs that make extensive use of dynamically allocated data structures such as lists and trees. Users need to provide a precondition, an inductive predicate in separation logic, to describe the input data structure. JSF then performs symbolic execution on the program to generate test cases, and use the precondition to guide its search. "Star" in the name refers to the separating conjunction in separation logic, and there is "Finder" since JSF is developed as an extension of the Java PathFinder framework. JSF was partially supported by the Google Summer of Code 2017 program.

Publications

Algorithmic details:

  • Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun, Shengchao Qin. Poster: Testing Heap-Based Programs with Java StarFinder. ICSE 2018. [PDF]
  • Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun, Shengchao Qin. Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation. Preprint. [PDF]

Applications:

  • Guolong Zheng, Quang Loc Le, ThanhVu Nguyen, Quoc-Sang Phan. Automatic Data Structure Repair using Separation Logic. JPF 2018. [PDF]

Installation

We provide two ways of installing JSF:

  • Virtual machine with Docker
  • Installation on local machine

Docker

Assuming you have Docker installed, simply run:

$ docker build -t star .
# Will take some time to build the image...
$ docker run -it star

Local Machine

To run Java StarFinder you need Java PathFinder and Symbolic PathFinder. Go to Java PathFinder website then install the packages jpf-core and jpf-symbc. After that, pull this repo and configure similar to jpf-symbc.

Usage

Try some examples in star/examples. Choose the files that end with Test.java and run it. It will generate test files that end with 1.java.

Questions and Issues

For common questions, bug reports, and feature requests, please use the JPF Google Group.