Homepage Sitemap Contact




Home « Service « Events

Taylor Expansion Diagrams - Application in Verification and Synthesis

Prof. Dr. Maciej Ciesielski


Date: 2004-12-17
Time: 13.00 Uhr s.t.
Place: Bremen, Uni Bremen
Meetingpoint: Raum 7230, MZH


Taylor Expansion Diagrams (TEDs) sind eine graphenbasierte Funktionsdarstellung - ähnlich zu BDDs. TEDs repräsentieren neben Booleschen Funktionen z.B. auch Funktionen über ganzzahligen Variablen. Genauso wie BDDs sind sie eine kanonische Darstellung von Funktionen und erlauben die Anwendung von Verknüpfungsalgorithmen direkt auf der Graphenstruktur. TEDs können für die Verifikation und die Synthese eingestzt werden. In meiner Forschung untersuche ich die Verifikation von Optimierungen und Codeerzeugungsverfahren, die aus Zwischenrepräsentationen mit statischer Einmalzuweisung (SSA=static single assignment) ausführbaren Maschinencode für neueste Prozessorarchitekturen (Itanium, ARM, TriMedia) erzeugen. Neben der Beschreibung der Spezifikation und Verifikation dieser optimierenden Codeerzeugung mit Hilfe des Theorembeweisers Isabelle/HOL stelle ich dar, wie die Implementierungskorrektheit solcher Optimierungsverfahren mit Programmprüfung sichergestellt werden kann. Dabei beschreibe ich auch einen Programmprüfer, den wir für einen Codegenerator in einem industriellen Projekt erstellt haben.



Link tp external SiteContact Person: Prof. Dr. Rolf Drechsler



zurück



Deutsch









Sitemap Kontakt

ISMVL2014 DUHDE