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

• Subject Area: Software Engineering and Programming Languages
• Term: from 2004 to 2007
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: CRC/Transregios
• Subproject of: TRR 14: Automatic Verification and Analysis of Complex Systems
• Co-Applicant Institution: Albert-Ludwigs-Universität Freiburg
• Applicant Institution: Carl von Ossietzky Universität Oldenburg
• Project Head: Professor Dr. Bernd Becker