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

Research interests

Compiler, verification, formal proofs (Isabelle/HOL)


Aktionsplan Informatik
Eliteförderprogramm fĂŒr Postdoktoranden

Advised thesis subjects

Diploma thesis
A Formal Semantics for the Pi Calculus (closed)
A Structural Operational Semantics for Static-Single-Assignment Languages (closed)
Studien thesis
(see german version) (closed)
Checker for Constant Propagation in Compilers (closed)
Coalgebraic Methods in Verification of optimizing Program transformations using Theorem provers (closed)
Maschinelle Verifikation der Codeerzeugung fĂŒr VLIW-Prozessoren (closed)
Mechanical Verification of Dead Code Elimination in SSA Representations (closed)
Verifikation unimodularer Schleifentransformationen (closed)

Theses worked on

Diploma thesis
A Formal Semantics for SSA Intermediate Representations in Isabelle/HOL (closed)
Studien thesis
Specification and Mechanical Verification of Constant Folding in Compiler Backends (closed)


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
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
Blech, Spezifikation und maschinelle Verifikation von Konstantenfaltung in Übersetzern
Glesner, Blech, Classifying and Formally Verifying Integer Constant Folding