longph1989/jpf-star

README

What is this repository for?

This is the source code for Java StarFinder project. Java StarFinder is a symbolic execution prototype based on separation logic. It can generate test cases for Java programs with data structures.

Version 1.0

How do I get set up?

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.

You can 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.

Note that you also need the solver S2SAT to run the examples. You should contact the authors of S2SAT to get the instructions how to compile and run the solver.

The author of S2SAT can be contacted via email: [email protected]

Who do I talk to?

You can contact repo admin if you have any questions.

Email: [email protected]