iSAT-Craig
Subproject |
H1/2 |
Categories |
Core algorithms, Model checker / solver for hybrid systems |
Overview |
The model checker iSAT-Craig can prove or disprove invariant properties of transition systems that contain non-linear dynamics. Such systems arise in the context of hybrid system verification. The model checker is build on top of the interval constraint solver iSAT that has been extended in order to compute Craig interpolants. These interpolants are used to over-approximate the set of reachable states. Once a fixed point of the reachable states is detected the invariant property has been proven to be valid and the procedure terminates. |
S. Kupferschmid and B. Becker. Craig interpolation in the presence of non-linear constraints. In Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2011), Lecture Notes in Computer Science (LNCS), 2011. To appear. |
|
iSAT-Craig Benchmarks |
|
Download |
Click here for the binary. |
Manual |
Just type ./iSAT-Craig on the command line to see how it can be used. |
Status |
Prototype |