Mihály Dobos-Kovács is a PhD student of Budapest University of Technology and Economics. His research focuses on using formal verification for test generation. Mihály is actively contributing the the Theta open source model checking framework, and participated in developing PLCverif, a tool developed at CERN targeting the formal verification of PLC code.