|
|
A New Approach to LL and LR Parsing
Martiček, Štefan ; Burgetová, Ivana (oponent) ; Meduna, Alexandr (vedoucí práce)
The aim of this thesis is to create a new effective parsing method via connection of LL and LR approaches. For demonstration purpose is made a new programming language according to the pattern of PHP. The language is separated into the sections and for constituent sections is chosen the most appropriate from the mentioned methods. For every section is created its own syntax analyser. The thesis provides a complete theoretical basis to construct every syntax analyser that has been used here. Finally, the syntax analysers are connected together and new method is practically presented. In conclusion, contributions of this work are discussed, such as the faster parser or the improved development. It also discusses usability of the designed method and suggestions for the next possible research in this area.
|
|
|
Synthesizing Non-Termination Proofs from Templates
Martiček, Štefan ; Fiedor, Tomáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
One of the properties that are most difficult to verify in the area of formal analysis is liveness. Proving non-termination of programs also belongs to the methods that verify this property. Our work describes the design and implementation of two algorithms checking non-termination. We inspire ourselves by already existing approaches, such as recurrence sets and over-approximation of loops with the use of invariants in the form of recurrence relations. The main challenge for us was an adaptation of these algorithms to the SSA (single static assignment) representation used in 2LS and the overall integration in our framework. We were able to unify the mentioned approaches into analysis of non-termination, which achieves the best results in comparison to the other tools that were compared at the SV-COMP 2017 competition.
|
|
|
Mobilní aplikace pro rozvrhovaní disciplín na dětském táboře
Holub, Ondřej ; Martiček, Štefan (oponent) ; Češka, Milan (vedoucí práce)
Práce se zabývá návrhem a tvorbou mobilní aplikace usnadňující plánování aktivit na dětském táboře na základě preferencí účastníků. Aplikace je implementována způsobem, který zajišťuje minimalizaci konfliktů preferencí s ohledem na dodatečná, uživatelem definovaná omezení. Pro efektivní zadávání vstupních dat je využito skenování karet účastníků, které obsahují QR kódy. Samotný proces hledání optimálního rozdělení je formalizován jako problém barvení grafu a je implementován s využitím metody větví a mezí. Vytvořený systém nevyžaduje pro své fungování žádné další zařízení, veškerý výpočet běží přímo na mobilním telefonu uživatele. Díky systému byl významně urychlen a zjednodušen proces plánování rozvrhů na dětských táborech.
|
|
|
Mobilní aplikace pro rozvrhovaní disciplín na dětském táboře
Holub, Ondřej ; Martiček, Štefan (oponent) ; Češka, Milan (vedoucí práce)
Práce se zabývá návrhem a tvorbou mobilní aplikace usnadňující plánování aktivit na dětském táboře na základě preferencí účastníků. Aplikace je implementována způsobem, který zajišťuje minimalizaci konfliktů preferencí s ohledem na dodatečná, uživatelem definovaná omezení. Pro efektivní zadávání vstupních dat je využito skenování karet účastníků, které obsahují QR kódy. Samotný proces hledání optimálního rozdělení je formalizován jako problém barvení grafu a je implementován s využitím metody větví a mezí. Vytvořený systém nevyžaduje pro své fungování žádné další zařízení, veškerý výpočet běží přímo na mobilním telefonu uživatele. Díky systému byl významně urychlen a zjednodušen proces plánování rozvrhů na dětských táborech.
|
|
|
Synthesizing Non-Termination Proofs from Templates
Martiček, Štefan ; Fiedor, Tomáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
One of the properties that are most difficult to verify in the area of formal analysis is liveness. Proving non-termination of programs also belongs to the methods that verify this property. Our work describes the design and implementation of two algorithms checking non-termination. We inspire ourselves by already existing approaches, such as recurrence sets and over-approximation of loops with the use of invariants in the form of recurrence relations. The main challenge for us was an adaptation of these algorithms to the SSA (single static assignment) representation used in 2LS and the overall integration in our framework. We were able to unify the mentioned approaches into analysis of non-termination, which achieves the best results in comparison to the other tools that were compared at the SV-COMP 2017 competition.
|
|
|
A New Approach to LL and LR Parsing
Martiček, Štefan ; Burgetová, Ivana (oponent) ; Meduna, Alexandr (vedoucí práce)
The aim of this thesis is to create a new effective parsing method via connection of LL and LR approaches. For demonstration purpose is made a new programming language according to the pattern of PHP. The language is separated into the sections and for constituent sections is chosen the most appropriate from the mentioned methods. For every section is created its own syntax analyser. The thesis provides a complete theoretical basis to construct every syntax analyser that has been used here. Finally, the syntax analysers are connected together and new method is practically presented. In conclusion, contributions of this work are discussed, such as the faster parser or the improved development. It also discusses usability of the designed method and suggestions for the next possible research in this area.
|
host ::
RSS.