Exakte Nichterreichbarkeitsanalyse für eingebetteten C Code durch arithmetisches Constraint Solving (T01#)

• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999

Das Transferprojekt zielt auf effiziente und präzise Erkennung nichterreichbarer Programmteile in reaktiver und regelungstechnischer eingebetteter Software mit hohem Anteil an Fließkommaarithmetik. Es betrachtet dabei sowohl aus Simulink und Stateflow generierte eingebettete C-Programme als auch nach den einschlägigen Regeln handkodierte eingebettete Software.

• DFG-Verfahren: Transregios (Transferprojekt)
• Teilprojekt zu: TRR 14: AVACS - Automatische Verifikation und Analyse komplexer Systeme
• Antragstellende Institution: Carl von Ossietzky Universität Oldenburg
• Mitantragstellende Institution: Albert-Ludwigs-Universität Freiburg
• Teilprojektleiter: Professor Dr. Bernd Becker; Professor Dr. Martin Fränzle