Verisoft ist ein nationales Verbundprojekt, das vom bmb+f gefördert wird. Projektpartner aus der Industrie und der akademischen Welt arbeiten in diesem Projekt gemeinsam daran, integrierte Computersysteme durchgehend formal zu verifizieren. Weitere Informationen befinden sich unter http://www.verisoft.de.

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.

In diesem Projekt möchten wir einen Betriebssystemkern spezifizieren und formal verifizieren. Der Betriebssystemkern unterstützt Memory Management ohne Shared Memory, I/O mit Geräten, Prozess-Management und synchrone Interprocess-Communication.

Das Ziel dieses Projektes is Design, Implementierung und formale Verifikation eines einfachen Betriebssystems (SOS). Das SOS ist ein privilegiertes Benutzerprogramm, das die Primitiven des VAMOS Mikrokerns nutzt, um anderen Benutzerprogrammen (den Applikationen) ein vollständiges Betriebssystem anzubieten.

In diesem Projekt formalisieren wir den FlexRay-Standard und designen einen FlexRay-Controller zum Einsatz in einem Automtive-System. FlexRay bietet zahlereiche Mechanismen zur Fehler-Korrektur und Clock-Synchornisation; außerdem garantiert es worst-case Kommunikationszeiten durch statisches Scheduling.