Příloha 8: Návrh habilitační komise na jmenování docentem Masarykova univerzita Fakulta Habilitační obor Fakulta informatiky MU Informatika Uchazeč Pracoviště Habilitační práce RNDr. Jan Strejček, Ph.D. Fakulta informatiky Masarykovy univerzity „From Infinite-State Systems to Translation of LTL to Automata" Habilitační komise Předseda Členové prof. RNDr. Ivana Černá, CSc. Masarykova univerzita - Fakulta informatiky prof. RNDr. Petr Jančar, CSc. Vysoká škola báňská - Technická univerzita Ostrava - Fakulta elektrotechniky a informatiky prof. Ing. František Plašil, DrSc. Univerzita Karlova v Praze - Matematicko-fyzikální fakulta prof. RNDr. Jan Slovák, DrSc. Masarykova univerzita - Přírodovědecká fakulta prof. Ing. Tomáš Vojnar, Ph.D. Vysoké učení technické v Brně - Fakulta informačních technologií Hodnocení vědecké kvalifikace uchazeče RNDr. Jan Strejček, Ph.D. pracuje na Fakultě informatiky Masarykovy univerzity od roku 2005 jako odborný asistent. Je absolventem Přírodovědecké fakulty MU (magisterský studijní program Matematika, absolutorium 2000) a Fakulty informatiky MU (magisterský studijní program Informatika, absolutorium 2001), dizertační práci Linear Temporal Logic: Expressiveness and Model Checking obhájil na FI MU v roce 2005, je držitelem ceny rektora MU za vynikající studijní výsledky z roku 2000 a ceny děkana FI MU z let 2001 (za výborné studijní výsledky) a 2007 (za vynikající disertační práci). Uchazeč se aktivně věnuje výzkumu ve třech oblastech, a to (1) vlastnosti lineární temporální logiky a jejich fragmentů, (2) vlastnosti nekonečně-stavových systémů a (3) analýza programů: metody hledání chyb a verifikace. Uchazeč je publikačně aktivní, je autorem či spoluautorem 18 publikací ve sbornících mezinárodních konferencí a 5 časopiseckých publikací. Podílel se na vzniku dvou databází {JAHODA, databáze verifikačních nástrojů, a CladbureDG: Classified Bug-Reports Database). Uchazeč dokládá 78 citací (bez autocitací, z toho 31 ve WOS) na publikované práce, což dokládá zájem mezinárodní odborné komunity o tyto výsledky. V rámci stáží o délce alespoň jednoho měsíce pracoval v minulosti na FMI, Universität Stuttgart (3 měsíce, 2005), a na LaBRI, Universitě Bordeaux (12 měsíců, 2005 - 2006). Zvané přednášky nebo tutoriály prezentoval na 5 fórech a odborných akcích v Evropě. Od roku 2010 byl členem (v jednom případě předsedou) programového výboru pěti mezinárodních odborných workshopů. Uchazeč se jako řešitel nebo spoluřešitel podílí či podílel na 9 projektech vědy a výzkumu v rámci GA ČR, AV ČR, MŠMT a FRVŠ. Na základě výše uvedených skutečností komise jednoznačně vyjadřuje názor, že se jedná o vědecky kvalitního uchazeče z oblasti informatiky, se zapojením do vědecké práce na mezinárodní úrovni. Závěr: Vědecká kvalifikace uchazeče odpovídá požadavkům standardně kladeným na uchazeče v rámci habilitačních řízení v oboru Informatika na MU. Hodnocení pedagogické způsobilosti uchazeče RNDr. Jan Strejček, Ph.D. pracuje na Fakultě informatiky Masarykovy univerzity od roku 2005 jako odborný asistent, v letech 2001 - 2005 působil jako vyučující FI MU formou dohody. Na FI MU uchazeč vede 3 přednášky - Automaty a gramatiky (IB102), Formal Verifícation Methods (IA159) a Matematické základy (IB112), a to od roku 2007 dosud. Cvičení pro studenty Bc i Mgr studia vede uchazeč samostatně od svého nástupu v roce 2005, celkově v 6 kurzech (Automaty a gramatiky, Vybrané kapitoly z teorie automatů, Computational Logic, Návrh algoritmů). Seminář vede v předmětu IA072 Seminár on Concurrency. Ke všem přednáškám připravil uchazeč rozsáhlé studijní materiály, z nichž zejména soubor odpovědníkových otázek (spolu s webovou službou pro jejich vyhodnocování) pro předmět IB102 je využíván velkým počtem studentů a výrazně přispěl ke zkvalitnění výuky předmětu. V posledních 5 letech uchazeč vedl 16 bakalářských prací, z toho 12 již bylo úspěšně obhájeno a jen 1 byla ukončena a neobhajována. Diplomových prací v tomto období vedl 7, z toho 3 byly úspěšně obhájeny. Dále je uchazeč školitelem-konzultantem 4 studentů PhD studia. Členem komisí pro SZZ na Bc i Mgr úrovni je uchazeč od šk. roku 2007/08. Závěr: Pedagogická způsobilost uchazeče odpovídá požadavkům standardně kladeným na uchazeče v rámci habilitačních řízení v oboru Informatika na MU. Hodnocení habilitační práce uchazeče Uchazeč předložil habilitační práci s názvem From Infinite-State Systems to Translation of LTL to Automata, která je souborem 4 časopiseckých a 7 konferenčních publikací. Oponenty habilitační práce kandidáta byli: • Prof. Jaco van de Pol, University of Twente, The Netherlands, odborník v oblasti modelování a analýzy bezpečnosti softwarových systémů za použití metod formální verifikace, • Prof. Philippe Schnoebelen, Laboratory for Specification and Verification (LSV), CNRS and ENS Cachan, France, odborník v oblasti formální verifikace systémů, se speciálním zaměřením na analýzu tzv. dobře strukturovaných systémů • prof. RNDr. Petr Jančar, CSc, Vysoká škola báňská - Technická univerzita Ostrava, Fakulta elektrotechniky a informatiky, člen habilitační komise, s odborným zaměřením na na otázky algoritmické rozhodnutelnosti a složitosti v oblasti verifikace systémů. Posudky všech tří oponentů byly veskrze kladné. Z hodnocení oponentů lze uvést např.: • Prof. Jaco van de Pol: „The papers are without exception very skillful, and mainly present the author's progress from 2001 - 2006 in solving dedicability problems for reachability, linear-time model checking and equivalence checking for infinite state systems, presented as subsystems of Process Rewrite Systems (PRS)." • Prof. Philippe Schnoebelen: „The collected papers contain theoretical and applied work of a very high level in a field, algorithmic verification, where the international competition is very active and quite demanding, and where very few researchers contribute significantly on both the theoretical and the applied sides. Furthermore, while Jan Strejček has chosen, and for the sake of thematic unity, to only present his work on PRS verification and translation of LTL to Buchi automata, there are a good number of additional contributions to the theory of verification which he could have put forward. His works has been published in some of the most visible and selective conferences of the field (TACAS, CONCUR, CSL, . . .). He has initiated new collaborations with foreign researchers of the highest calibre, and at the same time his list of coauthors also includes younger graduate students that he is apparently supervising in a productive way. For these reasons, I think that Jan Strejček has amply proved his excellence and maturity, and is fully deserving of the Habilitation diploma for which he is applying". • prof. RNDr. Petr Jančar, CSc: „Prácepřispívají do oblasti teorie automatizované verifikace systémů, v jednom případě se jedná i o práci zahrnující experimentální vyhodnocení. Většina prací rozšiřuje poznatky o vyjadřovací síle a otázkách rozhodnutelnosti základních problémů automatizované verifikace v kontextu tzv. procesových přepisovacích systémů. Kromě prací zařazených do souboru je J. Strejček (spolu)autorem i dalších kvalitních prací. Citace dokládají, že jeho práce je známa a oceňována v mezinárodní vědecké komunitě činné v oblasti automatizované (formální) verifikace, tedy v oblasti živého celosvětového výzkumu, jejíž důležitost je v situaci naší všudypřítomné závislosti na fungování složitých softwarových a hardwarových systémů zřejmá." Posudky na práci uchazeče dokladují vysokou kvalitu výsledků prezentovaných v práci. Závěr: Úroveň habilitační práce uchazeče odpovídá požadavkům standardně kladeným na habilitační práce v oboru Informatika na MU. Tři zástupci komise (Černá, Slovák, Vojnar) dne 25. 9. 2012 navštívili veřejnou přednášku uchazeče na téma symbolická exekuce a její praktická použití''', kde J. Strejček představil studovanou oblast, včetně dobrého úvodu do problematiky a představení základních řešených problémů a nejnovějších výsledků. Uchazeč také srovnal jím dosažené výsledky s dosavadním stavem výzkumu v předmětné oblasti a prezentoval pohled na další vývoj v oblasti a možné směry výzkumu. Přednáška prokázala dostatečnou vědeckou kvalifikaci a pedagogickou způsobilost uchazeče, standardně požadovanou v rámci habilitačních řízení v oboru Informatika na MU. Výsledek tajného hlasování komise počet členů komise 5 i počet členů komise přítomných hlasování "f počet odevzdaných hlasů Lj z toho kladných fy H záporných 0 neplatných Qf 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 úrovně habilitační práce uchazeče předkládá komise Vědecké radě Fakulty informatiky Masarykovy univerzity návrh /\ jmenovat uchazeče docentem v oboru Informatika. ] na zastavenwízení: prof. RNDr. Ivana Černá, CSc. / prof. RNDr. Petr Jančar, CSc. prof. Ing. František Plašil, DrSc prof. RNDr. Jan Slovák, DrSc. prof. Ing. Tomáš Vojnar, Ph.D