JBernstein: Exploration techniques for non-linear constraint checking

(assume-guarantee style):

Example (simple):
 
Example (assume-guarantee):

• Download and unzip the folder. 
• Switch the directory to the folder.
• Type java -jar JBernstein.jar to execute the program.
• In Windows, users may also double click JBernstein.jar 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 program.

A very quick instruction for constraint checking with the solver:

• Load existing examples 
• Simply select the combo box to load, and press the "Analyze" button.
• Alternatively, load some other examples from the menu bar using "File -> Load constraint".
  
• Work on your own examples
• Lines starting with ## are comments
• Specify the number of variables with keyword VAR
• Specify the coefficient with keyword COEF
• Specify the bound for each variable (the tool assumes that, e.g., given VAR equals 5, variables are named as x0, x1, x2, x3, x4) with keyword BOUND
• The value "Recursive expansion depth" specifies the maximum box refinement attempts for each variable to prove/disprove the constraint. 
• For a problem with <5 variables, it's safe to use value > 10 
• For a problem with more variables, all benchmarks 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.