Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

iSAT-Craig

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Felix Neubauer, M.Sc. Kontakt
ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur
Stefan Kupferschmid, Dr. Entwickler


Beschreibung

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

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



Publikationen
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