Název vaší oceněné dizertační práce zní Verification of Probabilistic Recursive Sequential Programs. Laik si těžko představí, co to vlastně je. Můžete to nějak přiblížit?
Základním cílem formální verifikace je ověřování správnosti daného systému vzhledem ke specifikaci. Takovým systémem může být třeba komunikační protokol, řídicí jednotka v letadle a podobně. Systém i specifikace správného chování jsou obvykle popsány pomocí vhodných matematických prostředků. Pravděpodobnostní rekurzivní sekvenční programy jsou jedním z matematických prostředků vhodných k popisování systémů, ve kterých hraje roli náhoda a které mají nekonečně mnoho stavů. Ve své dizertační práci jsem se zabýval návrhem algoritmů pro automatickou verifikaci těchto systémů.
Můžete víc popsat, jak je formální verifikace použitelná v praxi?
Jak jsem již naznačil, formální verifikace se může uplatnit všude tam, kde je nutné zajistit korektnost daného systému. Zásadní aplikace najdeme v letectví, kosmickém výzkumu, ve výrobě hardwaru a v mnoha dalších oblastech, kde se za chyby tvrdě platí – buď penězi, nebo dokonce životy. V poslední době se formální verifikace začíná využívat také v oblasti návrhu softwaru, tedy v oblasti, která obvykle není tak kritická. Většina velkých hardwarových a softwarových firem má vlastní pracoviště zabývající se formální verifikací.
Tato cena je pro mne významnou položkou v životopisu. Vzhledem k tomu, že hodlám pokračovat v akademické dráze, předpokládám, že bude hrát důležitou roli při výběrových řízeních, žádostech o granty a podobně.
Vaše životní krédo zní: Nejlepší je být lepší než ostatní. Zdá se, že se vám daří.
Děkuji. Toto krédo, které bohužel následuji zcela podvědomě, má i své stinné stránky. K těm patří například zvýšené množství lidí, kteří mi nemohou přijít na jméno, a neschopnost věnovat se více než jedné věci v jednom časovém období.
Pořád se ještě říká, že spousta mladých úspěšných vědců odchází do zahraničí. Bude to i váš případ?
Myslím si, že podmínky na Fakultě informatiky jsou dobré. Pokud dostanu možnost na fakultě zůstat, zůstanu. Jsem velmi spokojen s kolektivem, který se zformoval kolem institutu teoretické informatiky, a domnívám se, že máme ideální prostředí pro práci na kvalitním výzkumu.
Momentálně jste na stáži v Německu. Čím přesně se tam zabýváte?
V podstatě pracuji na stejném tématu jako v průběhu postgraduálního studia. Jedná se o poměrně mladou a dynamicky se rozvíjející oblast verifikace pravděpodobnostních systémů a her.
Mezi vaše koníčky patří windsurfing a býval jste dokonce úspěšný veslař.
Veslování už aktuální není. Na lodi jsem naposledy seděl, když mi bylo devatenáct let. Ale windsurfing je můj velký koníček, který ovšem vyžaduje enormní množství času. V praxi to vypadá zhruba tak, že několikrát za rok jedu na Nové Mlýny a jednou za rok na týden do Chorvatska.
Objevil jsem, že hrajete na klávesy v kapele Xychty. Fungujete ještě a hrajete dál? Co za hudbu hrajete?
Ano, stále hrajeme. Skupina se skládá převážně z absolventů Fakulty informatiky. Hrajeme čistě pro radost a žánr by se dal charakterizovat jako jednoduchý rock – takhle to aspoň nazval můj učitel klavíru. Není to žádné velké umění, ale připadá nám, že se naši posluchači alespoň pobaví.
