Die Allgegenw?rtigkeit von Mehrkern-Rechnerarchitekturen und Cloud Computing fordern von heutigen Software-Entwicklern, mehr und mehr Programmcode für komponenten-basierte Software zu schreiben. Dabei werden Komponenten entweder lokal nebenl?ufig ausgeführt oder laufen verteilt über ein Netzwerk und kommunizieren mittels asynchronem Nachrichtenaustausch untereinander. Da die so aus Komponenten gebauten Softwaresysteme auch immer h?ufiger in sicherheitskritischen Bereichen eingesetzt werden, müssen sie a priori robust und zuverl?ssig sein, sodass der mathematische Nachweis der Programmkorrektheit zu einer entscheidenden Aufgabe der Softwaretechnik wird.

Dieses Forschungsprojekt entwickelt formale Modelle für state-of-the-art Programmierparadigmen und APIs, wie beispielsweise Grand Central Dispatch, die es Programmierern erm?glichen, direkt asynchronen und nebenl?ufigen Programmcode zu schreiben. Ziel ist es, Softwaretechniker dabei so zu unterstützen, dass bereits durch die Art der Programmentwicklung die Korrektheit der Software garantiert ist.  Grundlegende Forschungsergebnisse hierzu basieren auf neuartigen, formalen Modellen der Automatentheorie und der Graphersetzungssysteme; das Projekt fokussiert auf die Entwicklung von (Semi-)Algorithmen zur automatischen Verifikation auf der Basis neuartiger Abstraktionstechniken. Langfristiges Ziel sind innovative algorithmische Ans?tze zur automatischen Synthese, insbesondere im Kontext der lokalen und verteilten Synthese von Schedulern, welche auf Ideen der Spieltheorie (z. B. nebenl?ufige Imperfect Information Games) und des maschinellen Lernens (z. B. Unsupervised Gray/Black-Box Learning) zurückgreifen.

Partner dieses Forschungsprojekts sind Dr. Grégoire Sutre (LaBRI Bordeaux, Frankreich), Dr. Tristan Le Gall (CEA Saclay, Frankreich), Prof. Jean-Francois Raskin und Dr. Gilles Geeraerts (ULB Brüssel, Belgien), sowie Dr. Chris Poskitt (ETH Zürich, Schweiz).

球探足球比分: Dr. Alexander Heu?ner

Publikationen:

• Geeraerts, G., Heu?ner, A. und Raskin, J.-F. Queue-Dispatch Asynchronous Systems. 13th Intl. Conf. on Application of Concurrency to System Design (ACSD 2013), S. 150-159, Barcelona, Spanien, Juli 2013. IEEE.
• Heu?ner, A., Le Gall, T., Sutre und G. McScM: A general framework for the verification of communicating machines. In C. Flanagan und B. K?nig, Hrsg., 18th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Band 7214 der Serie Lecture Notes in Computer Science, S. 478-484, Tallinn, Estland, M?rz 2012. Springer-Verlag.
• Heu?ner, A., Leroux, J., Muscholl, A. und Sutre, G. Reachability analysis of Communicating Pushdown Automata. Logical Methods in Computer Science, 8(3), 2012.