Constraint-basierte Verfikation hybrider Systeme (H02)

• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2008 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 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-Verfahren: Transregios
• Teilprojekt zu: TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme
• Internationaler Bezug: Tschechische Republik
• Antragstellende Institution: Carl von Ossietzky Universität Oldenburg
• Mitantragstellende Institution: Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik; Universität des Saarlandes
• Teilprojektleiter: Professor Dr. Ernst Althaus; Professor Dr. Bernd Becker; Professor Dr. Martin Fränzle; Professor Dr. Christoph Weidenbach
• Kooperationspartner: Dr. Stefan Ratschan