Travelled to:
1 × Taiwan
1 × Uruguay
2 × Germany
Collaborated with:
∅ S.Glesner S.O.Biha A.Poetzsch-Heffter L.Gesellensetter J.Leitner S.Mülling J.Huang A.Raabe C.Buckl A.Knoll
Talks about:
formal (3) code (3) isabell (2) generat (2) verif (2) base (2) hol (2) indistinguish (1) comparison (1) properti (1)
Person: Jan Olaf Blech
DBLP: Blech:Jan_Olaf
Contributed to:
Wrote 7 papers:
- DATE-2012-HuangBRBK #scheduling #smt
- Static scheduling of a Time-Triggered Network-on-Chip based on SMT solving (JH, JOB, AR, CB, AK), pp. 509–514.
- SAC-2011-Blech #encryption #logic #proving #security
- Proving the security of ElGamal encryption via indistinguishability logic (JOB), pp. 1625–1632.
- SEFM-2011-BlechB #coq #semantics #verification
- Verification of PLC Properties Based on Formal Semantics in Coq (JOB, SOB), pp. 58–73.
- COCV-2007-BlechP #code generation
- A Certifying Code Generation Phase (JOB, APH), pp. 65–82.
- COCV-J-2005-BlechGLM #code generation #comparison #correctness #higher-order #optimisation #proving
- Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.
- SEFM-2005-BlechGG #higher-order #verification
- Formal Verification of Dead Code Elimination in Isabelle/HOL (JOB, LG, SG), pp. 200–209.
- QAPL-2019-Blech #towards
- Towards Digital Twins for the Description of Automotive Software Systems (JOB), pp. 20–28.