Životopis

Vzdělání a akademická kvalifikace

• 2023: Kandidatura na děkana FIT VUT na období 1/2024--1/2028 (zisk 6/13 hlasů Akademického senátu FIT VUT). Kandidátská stránka (vize, motivace, program, tým, FAQ): html, pdf. Presentace na Akademickém shromáždění 16. 10. 2023: pdf.
• 2019--23: členství v panelu P103 GAČR.
• 2015, červen: zvaný přednášející doktorského kursu Automata-theoretic Methods for Infinite-State Verification na Fakultě informatiky, Technické univerzity ve Vídni.
• 2013, červen/červenec: zvaný profesor v laboratoři LIAFA, Université Paris Diderot/CNRS, Paříž, Francie.
• 2012: profesor v oboru výpočetní technika a informatika, FIT, VUT v Brně.
• 2007: docent v oboru výpočetní technika a informatika, FIT, VUT v Brně.
• 2005--2008: výzkumník zapojený (na částečný úvazek) sdružením CESNET do projektu Liberouter.
• 2005, červen/červenec: zvaný asistent v laboratoři LIAFA, Université Paris 7--Denis Diderot/CNRS, Francie.
• 2001--2003: postdok v laboratoři LIAFA, Université Paris 7--Denis Diderot/CNRS, Francie v rámci projektu ADVANCE.
• 1999-2007: odborný asistent na FIT (dříve FEI), VUT v Brně.
• 2001: Ph.D. v oblasti informatiky a kybernetiky, ÚIVT FEI VUT v Brně.
• 1996: Ing. v oblasti informatiky a výpočetní techniky, ÚIVT FEI VUT v Brně.

Přehled zaměstnání

Vědeckovýzkumná činnost

Výzkumné zájmy

• Statická analýza programů, zaměřená mimo jiné (ale nejen) na programy s ukazateli a dynamickými datovými strukturami, paralelními procesy či na výkonnost programů.
• Formální analýza a verifikace, obzvláště pro parametrické a nekonečně-stavové systémy.
• Dynamická analýza a testování, zejména pro paralelní programy.
• Automaty a logiky (nejen) pro potřeby verifikace.
• Viz také výzkumná skupina VeriFIT.

Rozšířené informace o publikacích

Publikace na DBLP

Záznam na Google Scholar

ha-index: 83

Ocenění vědeckou komunitou

• Zvané přednášky: ETAPS’22 "unifying speaker" (Mnichov) -- slajdy, ECOOP'15 Summer School (Praha), SAS'14 (Mnichov), INForum'14 (Porto), TTATT'13 (Hanoi), SOFSEM'11 (Nový Smokovec), INFINITY'10 (Singapur).
• Best theory paper award of ETAPS'10, cena udělena European Association for Theoretical Computer Science (EATCS).
• Ocenění za nejlepší články na konferencích CADE’19 a CIAA’08, ocenění za nejlepší články o nástrojích na konferencích ISSTA’18 a RV’12.
• 9 zlatých, 6 stříbrných, 5 bronzových medailích z International Software Verification Competition SV-COMP’12–22 s nástroji Predator, 2LS a Symbiotic.
• Bronzová medaile v rámci Human-Competitive Awards – “Humies” za metodu automatizovaného návrhu přibližných aritmetických obvodů založenou na kombinaci genetických algoritmů a formálních metod.
• Gödelova cena udělená v rámci FLoC 2014 Olympic Games za opakované úspěchy s nástrojem Predator v soutěži SV-COMP.
• 1 zlatá a 3 stříbrné medaile získané s nástroji SPEN a SLIDE na 1st International Competition of Separation Logic Decision Procedures SL-COMP'14 organisované v rámci SMT-COMP'14.
• Cena Siemens za disertační práci, 2001.

Aktivní působení v tuzemských a v zahraničních společnostech a organizacích

• Programové výbory konferencí a workshopů.
• Ediční rada časopisu STTT, Springer, téma Competitions and Challenges, od 12/2021.
• Spoluvedení programového výboru (spolu s Lijunem Zhangem) TACAS'19 -- 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Praha, ČR, 2019.
• Spoluvedení 13th Alpine Verification Meeting -- AVM'19, Brno, ČR, 2019. 
• Vedení soutěže SV-COMP 2018: 7th International Competition on Software Verification.
• Řízení workshopů v rámci CAV'10 -- 22nd International Conference on Computer-Aided Verification, FLoC 2010, Edinburgh, Velká Británie.
• Spoluvedení programového výboru (spolu s Peterem Habermehlem) INFINITY'08 -- 10th International Workshop on Verification of Infinite-State Systems, Toronto, Kanada.
• Ediční rada časopisu CAI, od 2/2005.
• Řídicí výbor MEMICS -- Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, ČR, do 2016.