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
 

Project Description

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