iSAT-Craig

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |

Der Model Checker iSAT-Craig kann sowohl invariante Eigenschaften eines Transitionssystems beweisen als auch widerlegen. Die Transitionssysteme dürfen dabei lineares und/oder nicht-lineares Verhalten haben. Solche Systeme treten bei der Verifikation sogenannter hybrider Systeme auf. Dieser Model Checker basiert auf dem Interval Constraint Solver iSAT, der hier um die Berechnung sogenannter Craigscher Interpolanten erweitert wurde. Mit Hilfe der Interpolanten können Überapproximationen erreichbarer Zustandsräume berechnet werden. Stellt iSAT-Craig fest, dass keine neuen Zustände mehr erreicht werden, so wurde gezeigt, dass die invariante Eigenschaft gültig ist und die Prozedur terminiert.

Benchmarks die mit diesem Werkzeug behandelt werden können, sind unter AVACS benchmark site zu finden.