JBernstein: Exploration techniques for non-linear
JBernstein is able to check polynomial constraint problems
of the following form (assume-guarantee style):
the file and open it with the Java Web Start Launcher, works
essentially for Windows and MacOS), or
- Download and unzip the folder.
- Switch the directory to the folder.
-jar JBernstein.jar to execute the program.
- In Windows, users may also double
to execute the program.
- In Linux or Mac OS, users can right click
the file, and select "open with JRE as runtime".
- Might need to set the property so that the
file is allowed to be executed as a
The solver is released under LGPLv3.
A draft submitted to CAV'13 (longer version, including a detailed statement on correctness) can be found here.
Screenshot of the tool
For disproving the following constraint
A very quick instruction for constraint checking with the
A note on performance: Every benchmark can be answered in 1 sec (under
normal desktop or laptop), including the Heart-Dipole example.
- Load existing examples
- Simply select the combo box to load, and
press the "Analyze"
- Alternatively, load some other examples from
the menu bar using "File -> Load constraint".
- Work on your own examples
- Lines starting with ##
- Specify the number of variables with keyword
- Specify the coefficient with keyword COEF
- Specify the bound for each variable (the
that, e.g., given VAR equals 5, variables are named as x0, x1, x2, x3,
with keyword BOUND
- The value "Recursive expansion depth"
maximum box refinement attempts for each variable to prove/disprove the
- For a problem with <5 variables,
it's safe to use value > 10
- For a problem with more variables, all
can be answered without using values greater than 5.
- In pre-load examples, these values are set
to let users
understand how many refinement steps are required.
- Users may always set the
value to 10 or higher.
- Assume-guarantee style properties can be found in the last item of the preload-examples or load from files.
- To overcome imprecision due to double, the user can specify a bound for strengthened property checking.
Screenshot for recording the time on PVS testsuite.
Contact: Chih-Hong Cheng [ cheng (dot) chihhong (at) gmail (dot) com
Back to EFSMT