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.

Publications

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.

Benchmarks

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