iSAT-Craig
| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen
|
| Lehrstuhl für Rechnerarchitektur | |
| Felix Neubauer, M.Sc. | Kontakt |
| ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur | |
| Stefan Kupferschmid, Dr. | Entwickler |
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.
|
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 |