Bounded Model Checking and Inductive Verification of Hybrid Systems (H 02)

• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2004 bis 2007
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999

Im Teilprojekt sollen Methoden für Bounded Model-Checking (BMC) und automatische induktiveVerifikation (IV) von hybriden diskret-kontinuierlichen Systemen entwickelt werden. Beide Beweismethodenwerden sehr erfolgreich im Bereich von diskreten Systemen angewendet und stoßen dort inbislang unerreichte Komplexitätsbereiche vor. Im Gegensatz dazu steckt BMC und IV für hybridediskret-kontinuierliche Systeme noch in den Anfängen. Diese Situation soll durch die Entwicklungvon heterogenen Beweisern, die verschiedenartige Beweismethoden in enger Integration kombinieren,entscheidend verbessert werden. Verknüpft werden sollen Methoden aus den Bereichen lineare Programmierung,Formale Verifikation von diskreten Systemen, SAT-Algorithmen, LP/ILP/MILPLöserund Heuristische Suche.

• DFG-Verfahren: Transregios
• Teilprojekt zu: TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme
• Mitantragstellende Institution: Albert-Ludwigs-Universität Freiburg
• Antragstellende Institution: Carl von Ossietzky Universität Oldenburg
• Teilprojektleiter: Professor Dr. Bernd Becker