Dnes, kdy bychom samoučící stroje rádi používali v medicíně či k řízení auta, je jejich správné a bezpečné fungování zásadní. Stejně jako u čipů nebo letadel nestačí systém párkrát otestovat, snahou je s matematickou přesností zcela vyloučit možné problémy.

Jan Křetínský ve své skupině vymýšlí matematické nástroje a programy, které toto umí, a to co nejvíce automaticky. Programy tak kontrolují jiné programy, roboty či neuronové sítě. Zabývá se teorií automatů, verifikací neuronových sítí a systémů umělé inteligence, ale také využitím technik strojového učení ve verifikaci.

Vystudoval informatiku a matematiku (ale také bakalářský program filozofie a lingvistiky) na Masarykově univerzitě v Brně. Doktorát získal i na Technické univerzitě v Mnichově. Po postdoktorské stáži v IST v Rakousku se vrátil do Mnichova v profesorské roli, kde setrval osm let. Poté přešel na svou alma mater.

Je autorem průkopnických prací, zabývá se také praktickými aplikacemi výsledků. Na kontě má mnoho významných publikací a těší se velkému respektu odborné komunity.