iSAT-Craig
| project staff | description | benchmarks | publications
|
| Chair of Computer Architecture | |
| Felix Neubauer, M.Sc. | Contact |
| former employee Chair of Computer Architecture | |
| Stefan Kupferschmid, Dr. | developer |
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.
Benchmarks that can be solved by this model checker can be obtained from the AVACS benchmark site.
|
Stefan Kupferschmid, Bernd Becker Craig interpolation in the presence of non-linear constraints Formal Modeling and Analysis of Timed Systems, 9th International Conference, FORMATS 2011 |