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
