Automatisierte Synthese von Programmausdrücken (AutoSynth)

In diesem forschungsvohaben sollen Verfahren zur automatischen Synthese on programmamausdricken entwickelt werden, um einee Art des systemwurfs zu etablien。Dabei是vorgesehen, dass der Entwickler静脉Programmskelett des spateren节日erstellt影响,韦尔奇zwar bereits阿莱Anweisungen des节日enthalt影响,河口Dabei manche Ausdrucke在窝Anweisungen als Syntheseziele经常lasst。Unter Beachtung zusätzlich gegebener Spezifikationen ermitteln dann die in diesem Forschungsvorhaben geplanten Verfahren hierfgr geeignete programmausdr<e:1>, so dass das somit entstandene vollständige Programm die gegebenen Spezifikationen erfllt。Die Untersuchungen diesesprojekts umfassen dabei Die syntaktische Repräsentation des Suchraums fr diesprogrammdr<e:1>, Die Anpassung bekannter Verfahren der controller - synthesis bzw。derspieltheorie, den Einsatz abstraker Interpretation sowie aktueller Deduktionsverfahren verunification and SMT-Verfahren zur Behandlung höherer Datentypen。Dabei soll mit einfachen Sicherheitseigenschaften begonnen werden, die dann in späteren Phasen des projects auf ω-reguläre Eigenschaften werden, so ass gängige Spezifikationen reaktiver system behandelt werden können。

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.