Universität Karlsruhe
Dipl.-Inform. Jan Olaf Blech

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
Login
Links