|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating
|
|
| |
|
|
Těžba uranu, její dopad na životní prostředí a rekultivace
Peterková, Alena ; Malíček, Jiří (vedoucí práce) ; Frouz, Jan (oponent)
Česká republika v minulosti patřila mezi významná území z hlediska těžby nerostných surovin. V období po druhé světové válce se stala velmi významným dobyvatelem uranové rudy, na kterou mnohonásobně vzrostla celosvětová poptávka díky rozvoji jaderné energetiky a masivní produkci nukleárních zbraní. V období osmdesátých let minulého století však zájem o uran poklesl a v devadesátých letech 20. století byly již téměř všechny uranové doly na našem území uzavřeny. Posledním místem těžby uranu byl důl Rožná, ve kterém bylo těženo až do roku 2017. V současné době probíhají na lokalitách rekultivační práce. Naplánování rekultivace pro dané území není však vždy jednoduchou záležitostí. Musí být brán v potaz způsob těžby, který byl na daném území prováděn, podloží, vzdálenost obydlí, podzemní vody, fauna a flóra okolí apod. Často jsou rekultivace prováděny nesprávným způsobem, a tím není dostatečně využit výjimečný potenciál biotopů zde vzniklých. Lidé mají tendence do obnovy krajiny silně zasahovat, jak už dodáváním živin, tak i vysazováním rostlinných druhů, a tím vytvářet intenzivní hospodářskou krajinu. Často si ovšem neuvědomují, že těžbou byla na lokalitě způsobena výrazná změna abiotických podmínek. Nově vzniklá stanoviště byla v mnohých případech osídlena vzácnými a ohroženými organismy, které jsou...
|
|
|
Těžba uranu, její dopad na životní prostředí a rekultivace
Peterková, Alena ; Malíček, Jiří (vedoucí práce) ; Frouz, Jan (oponent)
Česká republika v minulosti patřila mezi významná území z hlediska těžby nerostných surovin. V období po druhé světové válce se stala velmi významným dobyvatelem uranové rudy, na kterou mnohonásobně vzrostla celosvětová poptávka díky rozvoji jaderné energetiky a masivní produkci nukleárních zbraní. V období osmdesátých let minulého století však zájem o uran poklesl a v devadesátých letech 20. století byly již téměř všechny uranové doly na našem území uzavřeny. Posledním místem těžby uranu byl důl Rožná, ve kterém bylo těženo až do roku 2017. V současné době probíhají na lokalitách rekultivační práce. Naplánování rekultivace pro dané území není však vždy jednoduchou záležitostí. Musí být brán v potaz způsob těžby, který byl na daném území prováděn, podloží, vzdálenost obydlí, podzemní vody, fauna a flóra okolí apod. Často jsou rekultivace prováděny nesprávným způsobem, a tím není dostatečně využit výjimečný potenciál biotopů zde vzniklých. Lidé mají tendence do obnovy krajiny silně zasahovat, jak už dodáváním živin, tak i vysazováním rostlinných druhů, a tím vytvářet intenzivní hospodářskou krajinu. Často si ovšem neuvědomují, že těžbou byla na lokalitě způsobena výrazná změna abiotických podmínek. Nově vzniklá stanoviště byla v mnohých případech osídlena vzácnými a ohroženými organismy, které jsou...
|
|
|
Mikrobiální aktivita hlubinných miocénních sedimentů Sokolovské hnědouhlené pánve
Galertová, Renata ; Frouz, Jan (vedoucí práce) ; Kryštůfek, Václav (oponent)
Ve své práci jsem sledovala mikrobiální aktivitu v miocenních sedimentech získaných ze dvou různých hloubek - 30 a 150 metrů - v Lomu družba, který se nachází v Sokolovské hnědouhelné pánvi. Byly odebrány tři typy sedimentu: lamelární, amorfní a přechodný. Vzorky byly získány za sterilních podmínek a část ze vzorků přechodného jílovce byla ovlivněna přidáním glukózy, vlhčením a mrazením. Mým cílem bylo sledovat aktivitu původní hlubinné mikroflóry v různých hloubkách a její ovlivnění environmentálními faktory, kterým mohou být odtěžené jílovce po umístění na výsypky vystaveny. Mikrobiální činnost byla hodnocena za pomoci měření uvolněného CO2 (titrace). Naměřené hodnoty mikrobiální aktivity neukázaly výrazný rozdíl mezi respirací sedimentů různého stáří (hloubek), ale rozdíly mezi různými druhy sedimentů signifikantní byly, přičemž nejvyšší hodnoty byly naměřeny u lamelárního sedimentu. Ovlivnění vzorků potom do aktivity bioty přineslo odezvu, která napovídá, že společenstva velkých hloubek jsou limitována živinami. Protože aplikace glukózy nepřinesla až tolik výrazný efekt, je možné se domnívat, že tato společenstva jsou specializována na přítomnou fosilní organickou hmotu, kterou jsou schopna rozkládat, což má velký význam hlavně v počátečních stádiích rozvoje výsypek.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating
|
|
| |
host ::
RSS.