iSAT-LP
Subproject |
H1/2 |
Categories |
Core algorithms, Model checker / solver for hybrid systems |
Overview |
The model checker iSAT-LP can find so-called counterexamples in transition systems that contain linear and non-linear constraints. iSAT-LP combines the interval constraint solver iSAT and an LP solver (SoPlex 1.4.2). The LP solver has been integrated into iSAT to increase the performance on benchmarks that contain lots of linear constraints. We showed the effectiveness of this implementation by solving problem instances from the SMT-LIB. |
E. Althaus, B. Becker, D. Dumitriu, and S. Kupferschmid. Integration of an LP solver into interval constraint propagation. In Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing, 2011. To appear. |
|
iSAT-LP Benchmarks |
|
Download |
Click here for the binary. |
Manual |
Just type ./iSAT-LP on the command line to see how it can be used. |
Status |
Prototype |