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.

Tool Download

Click here to download the primitive version.