Super Brief Introduction
JavaSye is a symbolic execution engine for the Java platform. It is a part of the SAFELI framework. It has a primitive string constraint solver built in (algorithm described in the COMPSAC'07 paper). For handling regular replacement, you need the SUSHI constraint solver.
Installation tested only on WindowsXP + Cygwin. The tool needs Omega library for solving integer Presburger constraints.
To save trouble in installation, it might be convenient to extract the whole project under "C:\Xiang\Research\Projects\SAFELI\BCELExamples\Javasye". You might need to set up the library path of NetBeans correspondingly. You also need a copy of Javassit (version 3.6) deployed at "C:\Xiang\Research\Projects\SAFELI\BCELExamples\Javassit".
The project needs to be opened by NetBeans.
The unit test cases with the tool is the best way to learn how to use the tool.