|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
| |
|
|
Uranium mining, its impact on environment and recultivation
Peterková, Alena ; Malíček, Jiří (advisor) ; Frouz, Jan (referee)
In past, the Czech Republic was one of the most important areas for mineral resources mining. In the period after the Second World War, the country was a very important conqueror of the uranium ore, thanks to a massive production of nuclear energy and nuclear weapons. However, in the 1980s, the interest in uranium declined and in the 1990s almost all of the uranium mines in the country were closed. Rožná was the last place of uranium mining, but it was closed in 2017. Nowadays, there are reclamation works in these mining places. Planning of a reclamation for is not always simply. It is necessary to think about the account of the method of extraction, which was used in the territory, the subsoil, distance from dwellings, underground water, fauna and flora of the surrounding nature etc. The land reclamations are often done in the wrong way and therefore, the extraordinary potential of the landscape is not exploited. People have a strong tendency to interfere this landscape, for example by supplying nutrients for creating of an intensive agricultural landscape. They often do not realize that the mining caused a change of abiotic conditions. The newly created habitats are often inhabited by rare and endangered organisms, living in early succession stages and missing in the surrounding landscape....
|
|
|
Uranium mining, its impact on environment and recultivation
Peterková, Alena ; Malíček, Jiří (advisor) ; Frouz, Jan (referee)
In past, the Czech Republic was one of the most important areas for mineral resources mining. In the period after the Second World War, the country was a very important conqueror of the uranium ore, thanks to a massive production of nuclear energy and nuclear weapons. However, in the 1980s, the interest in uranium declined and in the 1990s almost all of the uranium mines in the country were closed. Rožná was the last place of uranium mining, but it was closed in 2017. Nowadays, there are reclamation works in these mining places. Planning of a reclamation for is not always simply. It is necessary to think about the account of the method of extraction, which was used in the territory, the subsoil, distance from dwellings, underground water, fauna and flora of the surrounding nature etc. The land reclamations are often done in the wrong way and therefore, the extraordinary potential of the landscape is not exploited. People have a strong tendency to interfere this landscape, for example by supplying nutrients for creating of an intensive agricultural landscape. They often do not realize that the mining caused a change of abiotic conditions. The newly created habitats are often inhabited by rare and endangered organisms, living in early succession stages and missing in the surrounding landscape....
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
| |
|
|
Vyhodnocení úspěšnosti lesnické rekultivace po těžbě černého uhlí v okolí Orlové
Cagašová, Kateřina
The present bachelor thesis is aimed at success rate evaluation of forestry re-cultivation in selected territories in the surroundings of the town Orlová and suggesting contingent measures thanks to which, it could be possible to improve the approach to technological re-cultivations followed by biological ones within the treatment of territories affected by underground coal mining. The evaluation paid special attention to an assessment of the site preparation before planting, woody plants used, crop and cover care, losses, length of the above-ground part and thickness of the trunk, tree-top and trunk shape, its vitality and impairments. The follow-up measures took into consideration specific features of the site and conditions of perspective growth of woody plants. The study exploited available materials and documentations which had been compiled since the beginning of planning of the re-cultivations themselves. Further findings were completed by measuring relevant dendrometrical values on the woody plants proper and through analysis of the site. Based on the evaluation of individual site researches there was a description of the present state of the covers done, their quality was assessed and suggestions of measures for the follow-up care were submitted. This study also pointed out some inconvenient steps including not always correct selection of the woody plant kinds, which did not take into proper consideration existing growth conditions in sites that had been formed from non equal landfillings of slag and topsoil with some of the re-cultivation events. In the end there was an evaluation of the accomplished technological actions performed in relation to the composition of species of the woody plants and the following planting thereof including suggestions of measures leading to improvements of quality of plantings and thus achieving quality target cover.
|
|
|
Influence of the surrounding vegetation on the vegetation succession on spoil heaps in the Kladno Region
DVOŘÁKOVÁ, Helena
The subject of this study was the effect of surrounding vegetation on the species composition of the dumps after black coal mining. The species data from dumps and their surroundings up to 100m were recorded during the vegetation seasons 2009-2011 and consequently analysed using ordination methods (DCA and CCA) and univariate statistics. The data on land cover and percent of the old forests (present in the surroundings in years 1836 -1852 up to 100m and 1km from the margins of the dumps) appeared to have significant effect on the present species composition of vegetation on the dumps.
|
guest ::
