This page is no longer updated. Please follow this link





Jan Olaf Blech

fortiss
Guerickestrasse 25
D-80805 Munich
phone : +49 89 360352230
email : joblech at gmail dot com

Publications


Jan Olaf Blech, Yliès Falcone, and Klaus Becker. Towards Certified Runtime Verification. 14th International Conference on Formal Engineering Methods. Kyoto, Japan, 2012. accepted

Jan Olaf Blech, Yliès Falcone, Harald Rueß, Bernhard Schätz. Behavioral Specification based Runtime Monitors for OSGi Services. Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2012. accepted

Jan Olaf Blech and Bernhard Schätz. Towards a Formal Foundation of Behavioral Types for UML State-Machines. 5th International Workshop UML and Formal Methods. Paris, France. August 2012.

Jan Olaf Blech, Dongyue Mou and Daniel Ratiu. Reusing Test-Cases on Different Levels of Abstraction in a Model Based Development Tool. Seventh Workshop on Model-Based Testing, Tallinn, Estonia. March 2012.

Jia Huang, Jan Olaf Blech, Andreas Raabe, Christian Buckl and Alois Knoll. Static Scheduling of a Time-Triggered Network-on-Chip based on SMT Solving. In Design, Automation and Test in Europe (DATE). Dresden, Germany, March 2012.

Jan Olaf Blech. Probabilistic Compositional Reasoning for Guaranteeing Fault Tolerance Properties. 15th International Conference On Principles Of Distributed Systems, vol. 7109 of LNCS, Springer, December 2011. (Extended version: J. O. Blech. On Compositional Reasoning for Guaranteeing Probabilistic Properties. March 2012. )

Jan Olaf Blech, Benoît Boyer, Thanh Hung Nguyen. On the Simulation of Time-Triggered Systems on a Chip with BIP.
http://arxiv.org/abs/1109.5505, 2011.


Jan Olaf Blech. A Tool for the Certification of Sequential Function Chart based System Specifications. 6th International Workshop on Systems Software Verification. Nijmegen, The Netherlands, August 2011. [pdf]

Jan Olaf BLECH and Sidi OULD BIHA. Verification of PLC Properties Based on Formal Semantics in Coq. 9th International Conference on Software Engineering and Formal Methods (SEFM), Montevideo, Uruguay, vol. 7041 of LNCS, Springer, 2011. [link]

Jia Huang, Jan Olaf Blech, Andreas Raabe, Christian Buckl and Alois Knoll. Analysis and Optimization of Fault-Tolerant Task Scheduling on Multiprocessor Embedded Systems. In International Conference on Hardware-Software Codesign and System Synthesis (CODES+ISSS). Embedded System Week. Taipei, Taiwan, Oct 2011.

Jia Huang, Jan Olaf Blech, Andreas Raabe, Christian Buckl and Alois Knoll. Reliability-Aware Design Optimization for Multiprocessor Embedded Systems. In 14th Euromicro International Conference on Digital System Design (DSD). Oulu, Finland. Aug 2011.

Jan Olaf Blech, Anton Hattendorf, Jia Huang. An Invariant Preserving Transformation for PLC Models. IEEE International Workshop on Model-Based Engineering for Real- Time Embedded Systems Design, 2011.
[link]


Jan Olaf Blech. A Tool for the Certification of PLCs based on a Coq Semantics for Sequential Function Charts.
http://arxiv.org/abs/1102.3529, 2011.


Jan Olaf Blech and Benjamin Grégoire. Certifying Compilers Using Higher-Order Theorem Provers as Certificate Checkers. Formal Methods in System Design, Springer, 2010.
http://www.springerlink.com/content/jtxr68281777u524/


Jan Olaf Blech. Proving the Security of ElGamal Encryption Via Indistinguishability Logic. ACM Symposium On Applied Computing (SAC), 2011. [link]

Jan Olaf Blech and Michaël PĂ©rin. Generating Invariant-based Certificates for Embedded Systems. ACM Transactions on Embedded Computing Systems (TECS). to appear

Jan Olaf Blech, Anton Hattendorf, Jia Huang. Towards a Property Preserving Transformation from IEC 61131-3 to BIP. http://arxiv.org/abs/1009.0817 http://arxiv.org/abs/1009.0817, 2010.

Jan Olaf Blech and Michaël Périn. Certifying Deadlock-freedom for BIP Models. Software and Compilers for Embedded Systems (SCOPES), Nice, France , 2009.
http://portal.acm.org/citation.cfm?id=1543820.1543832&coll=DL&dl=ACM


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. On Certifying Code Generation. Technical Report no. 366/07. University of Kaiserslautern, 2007.
http://kluedo.ub.uni-kl.de/frontdoor.php?source_opus=2144

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]

Membership in Program Committees

FMICS (Formal Methods for Industrial Critical Systems) 2011

Less Frequently Updated Stuff

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

From July 2008 till June 2010 I was a Post-Doc at VERIMAG Laboratory in France

Since July 2010 I am a researcher and project leader at fortiss.

back

Jan Olaf Blech --- last update: April 2011



This page is no longer updated. Please follow this link