Graduate Seminar

Ort: Raum S2-02 / E302
Datum und Zeit: 7. November 2007, 16:15-18:00

Moritz Sinn

Implementierung, Integration und Evaluation eines ACI-Matchingverfahrens

Die Arbeit befasst sich mit der Integration eines
Term-Matchingverfahrens modulo Assoziativität, Kommutativität und
Idempotenz (ACI-Matching) in das Verifikationswerkzeug VeriFun. Es wird
das Matching-Problem und seine Bedeutung für Theorem-Beweiser am
Beispiel von VeriFun vorgestellt. Aufbauend auf der Implementierung
wird
eine Evaluierung des ACI-Matchingverfahrens in VeriFun vorgenommen; es
werden Daten aus der Praxis vorgestellt, die die Vorteile belegen.