Jan Olaf Blech

Verimag, Centre Equation
2, avenue de Vignate
F-38610 GIERES
phone : +33456520432
email : joblech at gmail dot com

Publications


Jan Olaf Blech and Michaël Périn. Certifying Deadlock-freedom for BIP Models. Software and Compilers for Embedded Systems (SCOPES), Nice, France , 2009.

Jan Olaf Blech, Thanh-Hung Nguyen, and Michaël Périn. Invariants and Robustness of BIP Models. Workshop on Invariant Generation (WING), York, UK, 2009.

Jan Olaf Blech and Benjamin Grégoire. Using Checker Predicates in Certifying Code Generation. Compiler Optimization meets Compiler Verification (COCV), York, UK, 2009.
[pdf]

Jan Olaf Blech. Certifying System Translations Using Higher Order Theorem Provers. PhD-Thesis. ISBN 978-3-8325-2211-7. Logos-Verlag.

Jan Olaf Blech and Michaël Périn. On Certificate Generation and Checking for Deadlock-freedom of BIP Models. Verimag Technical Report number TR-2008-19, 2008.
[link]

Jan Olaf Blech and Michaël Périn. Towards Certifying Deadlock-freedom of BIP Models. Verimag Technical Report number TR-2008-1, Sep 2008.
[link]

Jan Olaf Blech and Benjamin Grégoire. Certifying Code Generation with Coq. Compiler Optimization meets Compiler Verification (COCV 2008), Budapest, Hungary, ENTCS, Elsevier, 2008.
[pdf]
This paper is accompanied by the following tool description paper:
Jan Olaf Blech and Benjamin Grégoire. Certifying Code Generation Runs with Coq:A Tool Description. Compiler Optimization meets Compiler Verification (COCV 2008), Budapest, Hungary, ENTCS, Elsevier, 2008.
[pdf]

Jan Olaf Blech, Ina Schaefer, and Arnd Poetzsch-Heffter. Translation Validation for System Abstractions. Runtime Verification (RV'07), Vancouver, Canada, LNCS volume 4839, Springer, 2007.
[pdf] [bib]

Jan Olaf Blech, Ina Schaefer, and Arnd Poetzsch-Heffter. On Translation Validation of System Abstractions. Technical Report no. 361/07. University of Kaiserslautern, 2007.
[pdf]

Jan Olaf Blech and Arnd Poetzsch-Heffter. A Certifying Code Generation Phase. Compiler Optimization meets Compiler Verification (COCV 2007), Braga, Portugal, ENTCS, Elsevier, 2007.
[pdf] [bib]

Marek Gawkowski, Jan Olaf Blech, and Arnd Poetzsch-Heffter. Certifying Compilers based on Formal Translation Contracts. Technical Report no. 355/06. University of Kaiserslautern, 2006.
http://kluedo.ub.uni-kl.de/frontdoor.php?source_opus=2038

Johannes Leitner, Sabine Glesner and Jan Olaf Blech. Coinductive Verification of Program Optimizations using Similarity Relations. Compiler Optimization meets Compiler Verification (COCV) 2006, Vienna, Austria, ENTCS, Elsevier, 2006.
[pdf]

Sabine Glesner and Jan Olaf Blech. Coalgebraic Semantics for Component Systems. In Architecting Systems with Trustworthy Components, LNCS volume 3938, Springer, 2006.

Jan Olaf Blech, Sabine Glesner, and Johannes Leitner. Formal Verification of Java Code Generation from UML Models. Fujaba Days, Paderborn, Germany, September 2005.
[pdf]

Jan Olaf Blech, Lars Gesellensetter, and Sabine Glesner. Formal Verification of Dead Code Elimination in Isabelle/HOL. Software Engineering and Formal Methods (SEFM), Koblenz, Germany, IEEE Computer Society Press, September 2005.
[pdf] [bib]

Jan Olaf Blech, Sabine Glesner, Johannes Leitner, and Steffen Mülling. A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. Compiler Optimization meets Compiler Verification (COCV), , Edinburgh, UK, Elsevier, April 2005.
[pdf] [bib]

Sabine Glesner and Jan Olaf Blech. Logische und softwaretechnische Herausforderungen bei der Verifikation optimierender Compiler. Proceedings der Tagung Software Engineering 2005, Lecture Notes in Informatics (LNI), March 2005.
[pdf] [bib]

Jan Olaf Blech and Sabine Glesner. A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL. Proceedings der 3. Arbeitstagung Programmiersprachen (ATPS) auf der 34. Jahrestagung der Gesellschaft für Informatik, Ulm, Lecture Notes in Informatics, September 2004.
[pdf] [bib]

Jan Olaf Blech. Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL. Universität Karlsruhe, March 2004. (Diplomarbeit)
[pdf] [bib]

Jan Olaf Blech. Spezifikation und maschinelle Verifikation von Konstantenfaltung in Übersetzern. Universität Karlsruhe, Mai 2003. (Studienarbeit)
[pdf] [bib]

Sabine Glesner and Jan Olaf Blech. Classifying and Formally Verifying Integer Constant Folding. Compiler Optimization meets Compiler Verification (COCV 2003), Warsaw, Poland, ENTCS, April 2003.
[pdf] [bib]

Some talks I have given

Teaching Experiences (since 2004)

winter term 2004/2005: Teaching Assistant "Übungen zur Vorlesung höhere Programmiersprachen" (higher-programming languages)

winter term 2005/2006: Teaching Assistant "Integrierte Lehrveranstaltung Software-Verifikation" (software verification)

winter term 2006/2007: Teaching Assistant "Software-Entwicklung 1" (software development 1)

summer term 2007: Teaching Assistant "Grundlagen des Software Engineering" (foundations of software engineering)

winter term 2007/2008: Teaching Assistant "Software-Entwicklung 1" (software development 1)

summer term 2008 (first half): Teaching Assistant "Specification and verification with higher-order logic"

Curriculum Vitae


I was born on January 24, 1979.

"School Education" from 1985 till 1998 in Göttingen.
In 1995 I spent a term at Truro College in Truro, England.
Abitur 1998 at Theodor-Heuss-Gymnasium in Göttingen

I started studying Computer Science in October 1999 at Karlsruhe University

I received my Vordiplom in September 2001

I worked as an "Info 2 Tutor" in 2001 at Institut für Logik, Komplexität und Deduktionssysteme (ILKD) in Karlsruhe.

From February 2002 till March 2004 I worked at the Institut für Programmstrukturen und Datenorganisation as a student research assistant in Karlsruhe.

I finished my Diploma-Thesis by March 2004

From April 2004 till September 2005 I was a PhD-student and worked as research- and teaching-assistant (wissenschaftlicher Mitarbeiter) at Karlsruhe University

From October 2005 till March 2006 I was a PhD-student and worked as research- and teaching-assistant (wissenschaftlicher Mitarbeiter) at the Technische Universität Berlin

From April 2006 till June 2008 I was a PhD-student and research and teaching-assistant (wissenschaftlicher Mitarbeiter) at the Technische Universität Kaiserslautern

Since July 2008 I am a Post-Doc at VERIMAG Laboratory in France

back

Jan Olaf Blech --- last update: March 2009