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