Arbeitsgebiete

Ãœbersetzer, Verifikation, formale Beweise (Isabelle/HOL)

Projekte

Abgeschlossen Aktionsplan Informatik Eliteförderprogramm für Postdoktoranden

Betreute Studien- und Diplomarbeiten

		Diplomarbeit
		Eine formale Semantik für den Pi-Kalkül (abgeschlossen)
		Eine strukturell operationale Semantik für static-single-assignment Sprachen (abgeschlossen)
		Studienarbeit
		Checker für Konstantenpropagierung in Compilern (abgeschlossen)
		Entwurf und Implementierung einer Schnittstelle für SSA-Sprachen (abgeschlossen)
		Koalgebraische Methoden in der maschinellen Verifikation vonoptimierenden Programmtransformationen (abgeschlossen)
		Maschinelle Verifikation der Codeerzeugung für VLIW-Prozessoren (abgeschlossen)
		Maschinelle Verifikation der Eliminierung toten Codes in SSA-Darstellungen (abgeschlossen)
		Verifikation unimodularer Schleifentransformationen (abgeschlossen)

Bearbeitete Studien- und Diplomarbeiten

		Diplomarbeit
		Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL (abgeschlossen)
		Studienarbeit
		Spezifikation und maschinelle Verifikation von Konstantenfaltung in Compiler Backends (abgeschlossen)

Veröffentlichungen

		2005
		Blech, Glesner, Leitner, Formal Verification of Java Code Generation from UML Models
		Blech, Gesellensetter, Glesner, Formal Verification of Dead Code Elimination in Isabelle/HOL
		Blech, Glesner, Leitner, Mülling, A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL
		Glesner, Blech, Logische und softwaretechnische Herausforderungen bei der Verifikation optimierender Compiler
		2004
		Blech, Glesner, A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL
		Blech, Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL
		2003
		Blech, Spezifikation und maschinelle Verifikation von Konstantenfaltung in Ãœbersetzern
		Glesner, Blech, Classifying and Formally Verifying Integer Constant Folding