Institute of Computer Languages
Compilers and Languages Group
| Date: | Friday, January 27th, 2006 |
|---|---|
| Time: | 15:00 (s.t.) |
| Location: | TU Wien, Elektrotechnik, Reithoffer Hörsaal, Gusshausstraße 25-29 (Altbau), 2. Stock |
Das Problem, die Wertegleichheit von Ausdrücken an einer Programmstelle festzustellen, ist bekanntermassen unentscheidbar. Dieses gilt selbst dann, wenn die Bedingungen des Programms nicht interpretiert werden. Aus diesem Grunde betrachtet man oft vereinfachte Modelle, in denen eine Teilklasse aller gültigen Gleichheiten entschieden werden kann. Ein besonders interessantes Szenario dieser Art bilden Gleichheiten zwischen Berechnungen, die unabhängig von den zugrunde liegenden Operatoreigenschaften gelten, sogenannte Herbrand-äquivalente Berechnungen.
Der Vortrag gibt zunächst einen Überblick über verschiedene klassische Verfahren in dem Bereich und diskutiert insbesondere Aspekte der Vollständigkeit und Komplexität. Anschliessend werden einige neuere Resultate beleuchtet. So wird gezeigt, dass Herbrand-äquivalente Berechnungen in polynomieller Zeit bestimmt werden können. Darüber hinaus wird ein neuer Anfrage-basierter Ansatz vorgestellt, mit dem beliebige positive Boolesche Kombinationen von Herbrand-Gleichheiten entschieden werden können, auch dann, wenn Tests auf Ungleichheit berücksichtigt werden.