Automatisierte Synthese von Programmausdrücken (AutoSynth)

• Applicant: Professor Dr. Klaus Schneider
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems
• Term: from 2010 to 2014
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 183475128

In diesem Forschungsvorhaben sollen Verfahren zur automatischen Synthese von Programmausdrücken entwickelt werden, um eine neue Art des Systementwurfs zu etablieren. Dabei ist vorgesehen, dass der Entwickler ein „Programmskelett“ des späteren Programms erstellt, welches zwar bereits alle Anweisungen des Programms enthält, aber dabei manche Ausdrücke in den Anweisungen als Syntheseziele offen lässt. Unter Beachtung zusätzlich gegebener Spezifikationen ermitteln dann die in diesem Forschungsvorhaben geplanten Verfahren hierfür geeignete Programmausdrücke, so dass das somit entstandene vollständige Programm die gegebenen Spezifikationen erfüllt. Die Untersuchungen dieses Projekts umfassen dabei die syntaktische Repräsentation des Suchraums für diese Programmausdrücke, die Anpassung bekannter Verfahren der Controller-Synthese bzw. der Spieltheorie, den Einsatz abstrakter Interpretation sowie aktueller Deduktionsverfahren wie Unifikation und SMT-Verfahren zur Behandlung höherer Datentypen. Dabei soll mit einfachen Sicherheitseigenschaften begonnen werden, die dann in späteren Phasen des Projekts auf ω-reguläre Eigenschaften erweitert werden, so dass gängige Spezifikationen reaktiver Systeme behandelt werden können.

• DFG Programme: Research Grants