Martin Strecker

Martin Strecker obtained a diploma in computer science from the TU Darmstadt and the INP Grenoble. He then worked as teaching and research associate at the University of Ulm, where he earned a PhD degree on the topic of program and proof development in Type Theory. After a stint in industry, he returned to academia (TU München) where he contributed to a major verification effort with the Isabelle proof assistant that resulted in the definition of a semantics for Java and the Java runtime system and, in particular, the verification of a Java source to Java bytecode compiler. Since his appointment as associate professor at the University of Toulouse, he has worked on provably correct model transformations and consistency of graph databases. At CCLAW, he participates in the definition and formal foundations of the L4 language and works on proof support for its reasoning engine.