Martin Fränzle

Since my doctorate, long before the term cyber-physical system even had been coined, I have been working on formal methods for modelling, verification, and synthesis of reactive, real-time, and hybrid dynamics in cyber-physical systems. My work spans the semantic foundations of high-level modelling and specification languages as well as decision problems and their application to rigorously verifying and synthesizing real-time and hybrid discrete-continuous systems, including settings subject to stochastic disturbances and human interaction. My contributions to the world-first extension of SAT-modulo-theory solving to the undecidable domains of arithmetic constraints involving transcendental functions have generated one of the very few commercially successful automatic verification tools for hybrid-state systems (iSAT, under distribution by BTC ES AG).