Detail práce

Advanced Methods for Synthesis of Probabilistic Programs

Diplomová práce Student: Stupinský Šimon Akademický rok: 2020/2021 Vedoucí: Češka Milan, doc. RNDr., Ph.D.
Název česky
Pokročilé metody pro syntézu pravděpodobnostních programů
Jazyk práce
anglický
Abstrakt

Pravdepodobnostné programy zohrávajú rozhodujúcu úlohu v rôznych technických doménach, ako napríklad počítačové siete, vstavané systémy, stratégie riadenia spotreby energie alebo softvérové produčkné linky. PAYNT je nástroj na automatizovanú syntézu pravdepodobnostných programov vyhovujúcich zadaným špecifikáciam. V tejto práci rozširujeme tento nástroj predovšetkým o podporu optimálnej syntézy a syntézy viacerých špecifikácií. Ďalej sme navrhli a implementovali novú metódu, ktorá dokáže efektívne syntetizovať parametre so spojitým definičným oborom ovplyvňujúce pravdepodobnostné prechody popri syntéze topológie programov, t.j., podporu pre syntézu topológie aj parametrov súčasne. Demonštrujeme užitočnosť a výkonnosť nástroja PAYNT na širokej škále prípadových štúdií z rôznych aplikačných domén ktoré majú uplatnenie v reálnom svete. Pri náročných problémoch syntézy môže PAYNT výrazne znížiť dobu behu až z dní na minúty a zároveň zaistiť úplnosť procesu syntézy.

Klíčová slova

automatizovaná syntéza, pravdepododnostné programy, Markovské modely, model checking

Ústav
Studijní program
Informační technologie a umělá inteligence, specializace Verifikace a testování software
Soubory
Stav
obhájeno, hodnocení A
Obhajoba
24. června 2021
Oponent
Průběh obhajoby

Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm A.

Otázky u obhajoby
  1. Jak "velké" programy je možné syntetiovat?
  2. Jak si představujete potenciálního uživatele Vašeho nástroje (čím se zabývá, k jakému úkolu bude chtít nástroj využít a jak).
  3. Jak by šla potenciálně ještě vylepšit výkonnost syntézy?
  4. Zkuste přesněji vymezit váš osobní přínos co se týče řešení probému a nástroje.
  5. Jaký programovací jazyk jste využil, jaké paradigma?
Komise
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT), předseda
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT), člen
Drábek Vladimír, doc. Ing., CSc. (UPSY FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
Citace
STUPINSKÝ, Šimon. Advanced Methods for Synthesis of Probabilistic Programs. Brno, 2021. Diplomová práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2021-06-24. Vedoucí práce Češka Milan. Dostupné z: https://www.fit.vut.cz/study/thesis/24077/
BibTeX
@mastersthesis{FITMT24077,
    author = "\v{S}imon Stupinsk\'{y}",
    type = "Diplomov\'{a} pr\'{a}ce",
    title = "Advanced Methods for Synthesis of Probabilistic Programs",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2021,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/24077/"
}
Nahoru