Martin Strecker

Affiliated Researcher


Martin Strecker obtained a diploma in computer science from the Technical University of 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. He then joined Etas GmbH, a subsidiary of the Bosch group, where he was responsible for the quality assurance of the Ascet-SD code generator, used in the embedded (in particular automotive) market. He then participated in the Verificard project at the TU M√ľnchen, which 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 joining the faculty of Toulouse University in 2004, he has been involved in several projects concerned with formalizations of domains specific languages in the embedded and aeronautics sector; the verification of concurrent Java programs; and provably correct model and graph transformations, with applications in graph databases. He is now collaborating with the Centre of Computational Law at Singapore Management University on issues on coherence of regulations and compliance. For more details and publications, please see or