Constaint-based Verification for Hybrid Systems (H02)

• Subject Area: Software Engineering and Programming Languages
• Term: from 2008 to 2015
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5485999

Das Projekt entwickelt Lösungsverfahren für große, gemischt Boolesch-arithmetische Constraintsysteme, um die Analyse symbolischer Darstellungen der Zustandsräume und der Dynamik hybrider Systeme zu ermöglichen. Constraint-Solving dient hier insbesondere der automatischen Erledigung der in der Analyse entstehenden Beweisverpflichtungen. Alleinstellungsmerkmal des Projekts ist seine Konzentration auf gut skalierende Lösungsverfahren in unentscheidbaren Fragmenten der Arithmetik, wie sie in hybriden Systemen aufgrund nichtlinearer Dynamik sowie Nicht-Ausdrückbarkeit erreichbarer Zustandsmengen in entscheidbaren Logiken regelmäßig auftreten.

• DFG Programme: CRC/Transregios
• Subproject of: TRR 14: Automatic Verification and Analysis of Complex Systems
• International Connection: Czech Republic
• Applicant Institution: Carl von Ossietzky Universität Oldenburg
• Co-Applicant Institution: Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik; Universität des Saarlandes
• Project Heads: Professor Dr. Ernst Althaus; Professor Dr. Bernd Becker; Professor Dr. Martin Fränzle; Professor Dr. Christoph Weidenbach
• Cooperation Partner: Dr. Stefan Ratschan