Hauptseite |
| Projektübersicht |
| Ziel dieses Projekts ist es, große Teile des interaktiven VAMP-Beweises zu automatisieren. Deshalb integrieren wir automatische Tools in Isabelle/HOL und benutzen diese, um so viele Lemmas und Teilaussagen wie möglich zu lösen. |
| Projektstatus |
| Der Model-Checker NuSMV ist in Isabelle/HOL über die Orakel-Schnittstelle eingebunden. Dabei werden CTL und LTL unterstützt. Mit Hilfe von NuSMV wurde ein sequentieller Prozessor verifitieziert. Alle Schaltkreise des Mirkoprozessors wurden ebenfalls mit NuSMV verifiziert. |
| Projektmitarbeiter |
|
Dr. Sergey Tverdyshev Pavel Emeliyanenko |
