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

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