Ort: Raum S2-02 / E302
Datum und Zeit: Dienstag, 24. Juni 2008, 16:25-18:00 Uhr

Markus Aderhold

Synthesis of Induction  Schemes for Procedures with Second-Order Recursion

Viele Algorithmen auf Datenstrukturen wie etwa Terme (endlich verzweigende Bäume) werden in natürlicher Weise mit Second-Order-Rekursion implementiert: Eine First-Order-Prozedur f enthält beispielsweise einen Aufruf "map(f, arguments(t))", um f mittels der Second-Order-Prozedur "map" rekursiv auf die direkten Teilterme von t anzuwenden. Um die Verifikation derartiger Algorithmen möglichst weitgehend zu automatisieren, ist die Synthese passender Induktionsschemata von zentraler Bedeutung.
Der Vortrag beschreibt zunächst die automatisierte Terminierungsanalyse von Prozeduren und zeigt anschließend, wie aus den beim Terminierungsbeweis gewonnenen Informationen geeignete Induktionsschemata synthetisiert werden können.

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang