JBernstein JBernstein: Exploration techniques for non-linear constraint checking


Description

JBernstein is able to check polynomial constraint problems of the following form
(assume-guarantee style):
spec

Example (simple):
 \forall x_0 \in [3,5], x_1\in [2,7] : 4x_0^2+5x_1^2 +3x_0x_1+2x_0+5 > 85
Example (assume-guarantee):
\forall x_0\in [0,1]: (6x_0-1>0\,\wedge\,3x_0-1<0)\,\rightarrow\,125x_0^3-175x_0^2+70x_0-8>0


Download

 (store the file and open it with the Java Web Start Launcher, works essentially for Windows and MacOS), or 

Download the JAR executable version and run the checker offline from SOURCEFORGE
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
 
\forall x_0 \in [3,5], x_1\in [2,7] : 4x_0^2+5x_1^2 +3x_0x_1+2x_0+5 > 85

Screenshot

A very quick instruction for constraint checking with the solver:

A note on performance: Every benchmark can be answered in 1 sec (under normal desktop or laptop), including the Heart-Dipole example.

Screenshot for recording the time on PVS testsuite.

Contact: Chih-Hong Cheng [ cheng (dot) chihhong (at) gmail (dot) com  ]
Back to EFSMT