Dobos-Kovács Mihály a Budapesti Műszaki és Gazdaságtudományi Egyetemen doktorandusza. Kutatási területe a formális módszerek felhasználása hatékony tesztgenerálási módszerek fejlesztésére. Mihály a Theta, egy nyílt forráskódú, moduláris formális verifikációs keretrendszer aktív fejlesztője, valamint részt vett a PLCverif, a CERN által fejlesztett, PLC kódok formális verifikációját támogató eszköz fejlesztésében is.