|
|
A New Approach to LL and LR Parsing
Martiček, Štefan ; Burgetová, Ivana (referee) ; Meduna, Alexandr (advisor)
Cílem této práce je vytvořit nový efektivní způsob syntaktické analýzy propojením LL a LR přístupů. Pro demonstrační účely je zhotoven nový programovací jazyk podle vzoru programovacího jazyka PHP. Tento jazyk je rozdělen na části, kde pro každou část je použita ta nejvhodnejší ze zmíněných metod. Jednotlivé metody jsou zde podrobněji popsané v kontextu dvou typů přístupů. Jedním z nich je syntaktická analýza shora dolů a tím druhým opačná verze, syntaktická analýza zdola nahoru. Pro každou separovanou část je vytvořen samostatný syntaktický analyzátor. Táto práce poskytuje kompletní teoretický základ k sestrojení všech zde použitých syntaktických analyzátorů a rozkladových tabulek. Nakonec jsou sestrojené analyzátory společne propojeny, což je úspěšné zakončení praktické demonstrace naší metody. V závěru jsou diskutovány dosažené výsledky práce jako efektivnejší druh syntaktické analýzy, modularita přístupu a podobně. Je zde také diskutovaná použitelnost navržené metody za účelem zefektivnení vývoje a rychlosti překladu. Jako poslední jsou uvedeny náměty pro další výzkum v této oblasti.
|
|
|
Synthesizing Non-Termination Proofs from Templates
Martiček, Štefan ; Fiedor, Tomáš (referee) ; Vojnar, Tomáš (advisor)
Jednou z nejsložitěji verifikovaných vlastností programů v oblasti formální analýzy je živost. K jedné z metod ověřujících tuto vlastnost patří i dokazování neukončitelnosti programů. Naše práce popisuje návrh a implementaci dvou algoritmů ověřujících neukončitelnost. Inspirujeme se již existujícími přístupy, jako jsou rekurentní množiny a nadaproximace cyklů s využitím invariantů ve tvaru rekurentních relací. Hlavní výzvu pro nás představovalo přizpůsobení těchto algoritmů SSA (single static assignment) reprezentaci použité v 2LS a jejich celková integrace v našem frameworku. Vzpomínané přístupy se nám podařilo spojit do analýzy neukončitelnosti, která dosahuje nejlepší výsledky v porovnání s existujícími nástroji, které byly srovnané na soutěži SV-COMP 2017.
|
|
|
Mobile Application for Scheduling Activities at Summer Camps
Holub, Ondřej ; Martiček, Štefan (referee) ; Češka, Milan (advisor)
The main goal of this thesis is to design and implement a mobile application assisting in scheduling activities at summer camps taking into account the preferences of camp participants. This is done in a way that ensures the minimization of conflicts with respect to user-defined constraints. QR code scanning is used as an effective method of data input. The main process of finding an optimal solution is formalized as a graph colouring problem and is implemented using the branch and bound method. The created system does not require any other device for its functioning, all the necessary calculations are being executed on a mobile phone of the user. This system has significantly accelerated and simplified the process of scheduling activities at summer camps.
|
|
|
Mobile Application for Scheduling Activities at Summer Camps
Holub, Ondřej ; Martiček, Štefan (referee) ; Češka, Milan (advisor)
The main goal of this thesis is to design and implement a mobile application assisting in scheduling activities at summer camps taking into account the preferences of camp participants. This is done in a way that ensures the minimization of conflicts with respect to user-defined constraints. QR code scanning is used as an effective method of data input. The main process of finding an optimal solution is formalized as a graph colouring problem and is implemented using the branch and bound method. The created system does not require any other device for its functioning, all the necessary calculations are being executed on a mobile phone of the user. This system has significantly accelerated and simplified the process of scheduling activities at summer camps.
|
|
|
Synthesizing Non-Termination Proofs from Templates
Martiček, Štefan ; Fiedor, Tomáš (referee) ; Vojnar, Tomáš (advisor)
Jednou z nejsložitěji verifikovaných vlastností programů v oblasti formální analýzy je živost. K jedné z metod ověřujících tuto vlastnost patří i dokazování neukončitelnosti programů. Naše práce popisuje návrh a implementaci dvou algoritmů ověřujících neukončitelnost. Inspirujeme se již existujícími přístupy, jako jsou rekurentní množiny a nadaproximace cyklů s využitím invariantů ve tvaru rekurentních relací. Hlavní výzvu pro nás představovalo přizpůsobení těchto algoritmů SSA (single static assignment) reprezentaci použité v 2LS a jejich celková integrace v našem frameworku. Vzpomínané přístupy se nám podařilo spojit do analýzy neukončitelnosti, která dosahuje nejlepší výsledky v porovnání s existujícími nástroji, které byly srovnané na soutěži SV-COMP 2017.
|
|
|
A New Approach to LL and LR Parsing
Martiček, Štefan ; Burgetová, Ivana (referee) ; Meduna, Alexandr (advisor)
Cílem této práce je vytvořit nový efektivní způsob syntaktické analýzy propojením LL a LR přístupů. Pro demonstrační účely je zhotoven nový programovací jazyk podle vzoru programovacího jazyka PHP. Tento jazyk je rozdělen na části, kde pro každou část je použita ta nejvhodnejší ze zmíněných metod. Jednotlivé metody jsou zde podrobněji popsané v kontextu dvou typů přístupů. Jedním z nich je syntaktická analýza shora dolů a tím druhým opačná verze, syntaktická analýza zdola nahoru. Pro každou separovanou část je vytvořen samostatný syntaktický analyzátor. Táto práce poskytuje kompletní teoretický základ k sestrojení všech zde použitých syntaktických analyzátorů a rozkladových tabulek. Nakonec jsou sestrojené analyzátory společne propojeny, což je úspěšné zakončení praktické demonstrace naší metody. V závěru jsou diskutovány dosažené výsledky práce jako efektivnejší druh syntaktické analýzy, modularita přístupu a podobně. Je zde také diskutovaná použitelnost navržené metody za účelem zefektivnení vývoje a rychlosti překladu. Jako poslední jsou uvedeny náměty pro další výzkum v této oblasti.
|
guest ::
