Příloha 10: Stanovisko hodnotící komise k návrhu na jmenování profesorem Uchazeč doc. RNDr. Jiří Barnat, Ph.D. Obor Informatika Složení komise: Předseda prof. RNDr. Mojmír Křetínský, CSc. Masarykova univerzita - Fakulta informatiky v Členové prof. RNDr. Petr Hliněný, Ph.D. Masarykova univerzita - Fakulta informatiky prof. RNDr. Petr Jančar, CSc. Vysoká škola báňská - Technická univerzita Ostrava - Fakulta elektrotechniky a informatiky doc. Ing. Petr Tůma, Dr. Univerzita Karlova v Praze - Matematicko-fyzikální fakulta prof. Ing. Tomáš Vojnar, Ph.D. Vysoké učení technické v Brně - Fakulta informačních technologií Stanovisko hodnotící komise: Na základě předložených dokumentů zhodnotila komise dosavadní vědecké a pedagogické působení uchazeče doc. RNDr. Jiřího Barnata, Ph.D., stejně jako jeho další činnost pro fakultu, univerzitu a akademickou komunitu vůbec. Po zralé úvaze podáváme následující zprávu. V roce 2000 promoval doc. RNDr. Jiří Barnat, Ph.D. s vyznamenáním na Fakultě informatiky MU v oboru informatika a oboru učitelství pro střední školy. Následně pokračoval jako doktorand na FI MU (školitel prof. RNDr. Luboš Brim, CSc), disertační práci obhájil v roce 2005. Poté působil na Fakultě informatiky jako odborný asistent a po úspěšné habilitaci v roce 2011 jako docent. Hodnocení vědecké kvalifikace uchazeče Text hodnocení (rozsah dle zvážení komise) Hlavní oblastí vědeckého zájmu uchazeče je formální verifikace a analýza paralelních a distribuovaných programů s efektivním využitím soudobých výpočetních prostředků. Této oblasti se uchazeč věnuje systematicky od počátku své vědecké kariéry, tj. zhruba 15 let. Mezi stěžejní algoritmické výsledky uchazeče patří především návrh nových paralelních algoritmů pro analýzu stavových prostorů programů a obecněji pro práci s rozsáhlými orientovanými grafy. Lze uvést například řešení pro komunitu dlouho otevřeného problému paralelní realizace metody Partial-Order Reduction, nebo vytvoření nového algoritmu pro paralelní dekompozici orientovaného grafu na silně souvislé komponenty nebo algoritmu pro paralelní řešení on-the-jly verifikace. Doc. Barnat dále působil v oblasti efektivního využití soudobých výpočetních prostředků, kde spolupracoval na adaptaci řady paralelních a distribuovaných algoritmů do prostředí se sdílenou pamětí, adaptaci algoritmů na vícejádrová zařízení (výpočty na GPU), nebo adaptaci algoritmů do výpočetního prostředí založeném na efektivním přístupu k externím diskům (tzv. IO Efficient Algorithms). Doc. Baniat se také zaměřil na problematiku verifikace paralelních programu zapsaných v reálných programovacích jazycích (C/C++), kde mezi významné výsledky lze zahrnout například novou melodii sdružováni mikroinstrukcí při interpretaci nízkoúrovňového kódu, plnohodnotnou realizaci verifikace programů s výjimkami, či unikátní datové struktury pro efektivní paralelní verifikaci vícevláknových programů. Rada teoretických výsledků doc. Barnata byla implementována a experimentálně vyhodnocena v softwarovém nástroji DIVINE, který vznikl na FI MU a je dosud rozvíjen pod jeho vedením. DIVINE je celosvětově unikátní a komunitou oceňovaný nástroj pro paralelní a distribuovanou verifikaci (LTL model checking) C/C++ a jiných programů. V poslední době se doc. Barnat věnuje také aplikacím metod formální verifikace na data-flow intenzivní systémy (vestavná zařízení), kde verifikace probíhá s využitím řešičů SAT a SMT. Za dobu svého působení publikoval doc. Barnat 23 článků v odborných časopisech, z nichž 12 je v časopisech s impaktním faktorem (z toho 1 zatím jen přijatý). Významným počinem je například článek v prestižním časopise Briefings in Bioinformatics (IF 9,283), který aplikuje formální ověřování modelu v oblasti analýzy a syntézy parametrů nad biologickými systémy. Neméně prestižní je další publikace v časopise IEEE Transactions on Automatic Control (IF 2.718), která byla za FI vybrána do RVVI Pilíře II za rok 2013. Dalšími prestižními časopisy, v nichž uchazeč publikoval, jsou Theoretical Computer Science či Journal of Parallel and Distributed Computing. Kromě časopiseckých publikací je doc. Barnat spoluautorem dalších 61 konferenčních příspěvků, z nichž tři jsou na konferencích nejvyšší světové (tzv. flagship neboli A*) kvality Computer Aided Verification CAV a dalších 10 na špičkových světových konferencích (tzv. A) jako ASE, ICECCS, ATVA, TACAS, 1PDPS, CDC. Na tomto místě je vhodné poznamenat, v informatice obecně je zvykem nejvyšší pozornost věnovat publikacím výsledků ve špičkových recenzovaných konferencích, které se však podle metodiky hodnocení výzkumu objevují v seznamu článků ve sbornících a nemají impakt faktor. Na práce doc. Barnata je doloženo 739 ohlasů, z nichž 128 je evidováno v databázi Web of Science (jejímž problémem je nedobré a velmi opožděné pokrytí CS konferencí) a zbylé jsou dodány vlastním seznamem. Mezi uvedenými ohlasy na práce uchazeče nejsou vedeny žádné ohlasy pocházející ze závěrečných prací studentů FI. Doc. Barnat byl řešitelem jednoho post-doktorského, a je aktuálně řešitelem jednoho standardního projektu GAČR, byl spoluřešitelem evropského projektu CRYSTAL společné technologické iniciativy Artemis, a je aktuálně spoluřešitelem evropského projektu AMASS společné technologické iniciativy ECSEL. Navíc doc. Barnat významně přispěl k úspěšnému řešení řady dalších projektů řešených na FI MU jako člen řešitelského týmu. Odbornou kvalitu uchazeče dokládají také zvané přednášky, které uchazeč za své dosavadní působení pronesl. Jsou to mimo jiné zvané přednášky na zahraničních univerzitách (Aalborg, Dánsko; Boston, USA) a výzkumných pracovištích (INRIA Rhône-Alps, Francie; CWI, Nizozemí; IST, Rakousko), ale také zvané přednášky na mezinárodních workshopech a konferencích. Odbornou kvalitu doc. Barnata dosvědčují také profesor Jaco van de Pol z Univerzity v Twente a profesorka Marta Kwiatkowska z Univerzity v Oxfordu ve svých doporučujících dopisech. Zmiňují například, že doc. Barnat publikoval na oborově specifických A* konferencích a v prestižních časopisech, nebo že doc. Barnat je vysoce viditelný ve vědecké komunitě, což je doloženo jeho přítomností v programových výborech řady kvalitních mezinárodních konferencí a workshopů. Celkově lze tedy hodnotit vědecké působení doc. Barnata jako velmi úspěšné, a to jak do počtu a kvality výzkumných výsledků, tak i z hlediska netriviálního impaktu na komunitu doloženého zvanými přednáškami, přítomností v programových výborech, vybudováním vlastní vědecké školy v oblasti verifikace (blíže v další části) a řadou citací. Závěr: Vědecká kvalifikace uchazeče odpovídá požadavkům standardně kladeným na uchazeče v rámci řízení ke jmenování profesorem v oboru Informatika na MU. Hodnocení pedagogické způsobilosti uchazeče Text hodnocení (rozsah dle zvážení komise) Pedagogické působení uchazeče je svým rozsahem a kvalitou příkladné. Doc. Barnat působí pedagogicky na Fakultě informatiky jako akademický pracovník od roku 2005, pravidelnou výuku však vedl již jako student, a to od roku 2000. Jako odborný asistent (2005-2011) vedl výuku v rozsahu 8-10 vyučovacích hodin týdně, jako docent pak 6-8 hodin týdně. Během svého pedagogického působení uchazeč připravil tři nové přednášky (Úvod do validace a verifikace, Návrh a implementace paralelních systémů, System Verification and Assurance) a významně inovoval přednášku Neimperativní programování. Také se podílel na vytvoření sbírky příkladů pro cvičení ke klíčovým předmětům bakalářského (dříve pětiletého magisterského) studia (Formální jazyky a automaty I a II), a založil projektový předmět Projekt z programování paralelních aplikací. O kvalitě výuky doc. Barnata, svědčí mimo jiné také udělení Ceny rektora pro vynikající pedagogy Masarykovy Univerzity, kterou doc. Barnat získal roce 2015. Cena je udělována na základě hodnocení studentů ajejich zpětné vazby. Během svého akademického působení vedl a vede doc. Barnat 49 bakalářských a 21 diplomových prací, z nichž drtivá většina byla úspěšně obhájena nebo jsou dosud v běhu. Jako školitel dovedl doc. Barnat dva doktorandy k úspěšné obhajobě, předtím působil u dvou úspěšně zakončených doktorských studií v roli konzultanta. V současnosti vede jednoho doktoranda. Dále doc. Barnat vedl projekt Fondu Rozvoje Vysokých Škol, dva projekty FRMU a několik studentských projektů děkana FI. Dlouhodobě působí jako člen a posledních několik let i jako vedoucí výzkumné laboratoře ParaDiSe na Fakultě informatiky, na jejíž činnosti se každoročně podílí netriviální počty bakalářských a magisterských studentů fakulty a která kromě výchovy studentů produkuje významné vědecké výsledky světové úrovně. Doc. Barnat je členem oborové komise pro doktorské studium oboru Informatika od roku 2012 a členem komisí pro SZZ bakalářského a magisterského studia programů Informatika a Aplikovaná informatika od roku 2007. Ohledně kvality vedení doktorských studentů se také explicitně vyjadřuje doporučující dopis prof. Kwiatkowské z Oxfordu, která na základě své spolupráce s bývalými doktorandy uchazeče píše: ... the quality of graduate training he (doc. Barnat) provided is excellent. Doc. Barnat několik let působil jako garant bakalářského oboru Paralelní a Distribuované Systémy vyučovaném na Fakultě informatiky MU, který významně aktualizoval, a nyní působí jako Proděkan pro studijní programy na Fakultě informatiky MU a jako garant oboru Aplikovaná informatika. Jedná se o výrazného pedagoga Fakulty informatiky, který se v posledních letech velmi viditelným způsobem podílí na celkovém pedagogickém směřování fakulty. Závěr: Pedagogická způsobilost uchazeče odpovídá požadavkům standardně kladeným na uchazeče v rámci řízení ke jmenování profesorem v oboru Informatika na MU. Hodnocení uchazeče jako význačné a uznávané vědecké osobnosti v daném oboru Text hodnocení (rozsah dle zvážení komise) Doc. Barnat je nepochybně již po několik let vůdčí osobností výzkumného týmu laboratoře ParaDiSe na Fakultě informatiky, jejíž velký význam v oblasti formální verifikace na světové úrovni dokládají nejen mnohé publikace a citace ve špičkových konferencích a časopisech, ale opakovaně jej zmiňují také doporučující dopisy prof. Kwiatkowské a prof. van de Pola. Doc. Barnat je spoluautorem jedné z nejvíce citovaných prací publikovaných na workshopu SPIN, což je prestižní, oborově velmi úzké fórum zaměřené na praktickou formální verifikaci. Dále pravidelně působí v programových výborech mezinárodních konferencí s relevantní tématikou, jako jsou například ASCD, SPIN, SEFM a další. Mimo jiné doc Barnat získal Best páper award za článek publikovaný na mezinárodní konferenci HASE a pronesl zvanou přednášku o způsobu výuky paralelního programování na americkém fóru pro výuku v této oblasti. O kvalitách uchazeče nepochybují ani oba přiložené doporučující dopisy špičkových světových expertů v oblastech formální verifikace. Profesorka Kwiatkowska z Oxford University ve svém doporučujícím dopise píše například: Dr Barnat 's most important contribution, in my view, is to the development of parallel and distributed algorithms for LTL (Linear Temporal Logic) model checking, including multi-core and GPU accelerated algorithms......................... Within my research field (automated verification), Masaryk University stands out in comparison with Eastern European universities in terms in the high success rate of acceptances in top publication venues, notably world leading conferences T AC AS and CAV. Masaryk's success is to a large extent due to the commitment and leadership of Dr Barnat. Profesor van de Pol z Twente University zase píše, mimo jiné: / have known Dr. Jiri Barnat for more than 10 years, and I regard him as an excellent researcher in the field of formal methods and automated software verification, and in particular as a specialist on the design and experimental evaluation of high-performance parallel and distributed model checking algorithms...................... Dr. Barnat showed leadership in the international community by organizing a series of workshops PDMC on Parallel and Distributed Model Checking, being all-time PC member and several times PC-chair. Z uvedeného je zjevné, že doc. Barnat je význačnou a světově uznávanou vědeckou osobností a významně se zasluhuje o profilování a rozvoj oboru formální verifikace ve směru paralelní a distribuované verifikace vhodné pro praktické nasazení na reálný programový kód v průmyslových aplikacích. Zároveň je doc. Barnat vůdčí osobností mezinárodně velmi úspěšného výzkumného týmu laboratoře ParaDiSe na Fakultě informatiky. Závěr: Uchazeč je význačnou a uznávanou vědeckou osobností v daném oboru. Významně se zasluhuje o profilování a rozvoj tohoto oboru. Představuje jednu z vůdčích osobností vědecké školy nebo výzkumného týmu v oboru. Závěr Dne 19.4.2016 přednesl doc. RNDr. Jiří Barnat, Ph.D. před odbornou veřejností svoji přednášku "10 let DIVINE - Co bylo, je a bude", ve které poukázal na historii vývoje nástroje DIVINE, dosažené relevantní výsledky a nastínil směr vývoje pro následující období. Přednáška se setkala s velmi příznivým ohlasem. Komise konstatuje, že doc. RNDr. Jiří Barnat, Ph.D. splňuje všechny zákonné podmínky a shodla se na doporučení, aby byl jmenován profesorem pro obor Informatika v tajném hlasování. Výsledek tajného hlasování komise počet členů komise 5 počet členů komise přítomných hlasování 4 počet odevzdaných hlasů 4 z toho kladných 4 záporných 0 neplatných 0 Návrh komise Na základě výsledku tajného hlasování následujícího po zhodnocení vědecké kvalifikace, pedagogické způsobilosti a profilu uchazeče jako význačné a uznávané vědecké osobnosti předkládá komise Vědecké radě Fakulty informatiky Masarykovy univerzity návrh X jmenovat uchazeče profesorem v oboru Informatika. ] na zastavení řízení. Brno, dne prof. RNDr Mojmír Křetínský, CSc. (podpis) prof. RNDr. Petr Hliněný, Ph.D. (podpis) prof. RNDr. Petr Jančar, CSc. (podpis) doc. Ing. Petr Tůma, Dr. (podpis) prof. Ing. Tomáš Vojnar, Ph.D. (podpis) ' // q