Thesis (M. Sc.)--University of Canterbury, 2008. / Typescript (photocopy). Includes bibliographical references (p. 118-119). Also available via the World Wide Web.

Contract inference consists in automatically computing contracts that formally describe the behaviour of program functions. Contracts are used in deductive verification, which is a method for verifying whether a system behaves according to a provided specification. The Saida plugin in Frama-C is a contract inference tool for C code. This thesis explores an extension to the Saida plugin which allows support for pointers and heap allocations. The goal is to evaluate to what extent model checking tools can be used to infer contracts for deductive verification of programs that use pointers and heap allocations. This is done by proposing a translation strategy to convert contracts containing heap expressions, generated by the model checker TriCera, into ACSL, a specification language used by Frama-C. An implementation of this translation is evaluated using a set of verification tasks. The results demonstrate that the inferred contracts are sucient to verify simple code samples, including features such as recursion, aliasing, and manipulation of heap-allocated structs. However, the results also reveal cases where the contracts are too weak, although more information could be extracted in the translation. It is concluded that model checking tools can infer contracts for deductive verification of programs with pointers and heap allocations, but currently to a limited extent. Several improvements to the translation strategy are proposed for future work. / Kontrakthärledning består i att automatiskt härleda kontrakt, vilka formellt beskriver funktioners beteende i program. Kontrakt används för deduktiv verifiering, vilket är en metod för att verifiera huruvida ett system beter sig enligt en given specifikation. Pluginet Saida i Frama-C är ett verktyg för kontrakthärledning för C-kod. Denna avhandling undersöker en vidareutveckling av Saida som möjliggör stöd för pekare och heap-allokeringar. Målet är att utvärdera i vilken utsträckning modellprovningsverktyg kan användas för att härleda kontrakt för deduktiv verifiering av program som använder pekare och heap-allokeringar. Detta görs genom att presentera en översättningsstrategi för att konvertera kontrakt som involverar heaputtryck, genererade av modellkontrollverktyget TriCera, till ACSL, vilket är ett specifikationsspråk som används av Frama-C. En implementation av denna översättning utvärderas med hjälp av en samling verifieringsproblem. Resultaten visar att de härledda kontrakten är tillräckliga för att verifiera enkla verifieringsproblem, med koncept som rekursion, aliasing och manipulation av heap-allokerade structs. Resultaten visar även fall då kontrakten är för svaga, men där mer information skulle kunna utvinnas i ¨översättningen. Slutsatsen dras att modellprovningsverktyg kan härleda kontrakt för deduktiv verifiering av program med pekare och heap-allokeringar, men för närvarande i begränsad utsträckning. Flera förbättringar av översättningsstrategin föreslås för framtida vidareutveckling.

Plant diversity and selected soil parameters from 36 sites placed on brown coal mining spoil heaps were analyzed and compared. Spontaneously revegetated or technically reclaimed spoil heaps of different age were situated in brown coal mining district of eastern Most basin in north western part of the Czech republic. Samples were sorted in groups according to vegetation growth and type. Plant diversity increases during succession development and is higher on non-reclaimed sites than reclaimed sites, where diversity decreases with time. Soil bulk density decreases during succession on all sites. Soil pH is decreasing too and this process is faster on spontaneously revegetated sites. Old successional forest type sites have very acid soils probably due to properties of original mineral matrix. Thickness of organic horizon and A horizon is increasing during succession and they appear in mid-aged sites first. Content of soil organic carbon is increasing continuously. Non-reclaimed sites reach higher contents, mainly because of higher content of fossil organic matter in spoil mineral matrix. Keywords: vegetation succession, soil development, reclamation, brown coal mining heaps

Extraction of mineral resources causes landscape degradation and the aim of reclamation efforts is to restore ecosystems. Our research was carried out on spoil heaps after brown coal mining near Sokolov (Czech Republic). We compared twenty years old spontaneously developed sites and reclaimed sites afforested by alders Alnus glutinosa and A. incana. Biomass and nutrient budget were evaluated for herbs and woody plants, separately for species Salix caprea, Populus tremula and Alnus glutionosa. Alder showed significantly higher concentrations of nitrogen and carbon compared to other tree species. The total amount of biomass, carbon and nitrogen was higher on reclaimed sites whereas phosphorus was more represented on spontaneously developed sites. Most of nitrogen was accumulated in the below-ground tree biomass and the largest amount of phosphorus was in the above-ground tree biomass. Woody plants of non-reclaimed sites produced more litter whilst litter of alder stands showed a higher concentration of nitrogen. Higher values of biomass, carbon and nitrogen of reclaimed sites were probably achieved through alder ability to fix atmospheric nitrogen.

Sometimes percentile points cannot be determined analytically. In such cases one has to resort to Monte Carlo techniques. In order to provide reliable and accurate results it is usually necessary to generate rather large samples. Thus the proper organization of the relevant data is of crucial importance. In this paper we investigate the appropriateness of heap-based data structures for the percentile point estimation problem. Theoretical considerations and empirical results give evidence of the good performance of these structures regarding their time and space complexity. (author's abstract) / Series: Forschungsberichte / Institut für Statistik

Abundance and species composition of soil rotifer communities was investigated in two seasons and six sites on dumps in the Sokolov mining area (Czech Republic). Every site was split into three plots, which differed in toxicity for vegetation and chemical composition of spoil material. The ability of soil rotifers to live in environment of spoil materials and the effect of pollution were studied in field conditions. According to results, abundance and species composition did not correspond to chemical environmental characteristics. Species composition of rotifer communities was affected by environmental variables such as vegetation, more likely than direct effect of chemical composition of spoil material.

The content of this diploma thesis is to verify of possibilities for remediation spoil heap toxicity in Sokolov area, by the help of creating biological crusts. The main question of this work is the possibility of using algae to create biological crust on toxical substrates, which could improve the properties of substrates and contribute to the acceleration of succession. The correctness of this theory was tested using two tests on toxic soils in spoil heaps near Sokolov. In the first test (laboratory test) have been chosen two of the soils and the higher plants, in most cases, even did not germinate. That is why we decided to verify the second option to create biological crust in these phytotoxic soils. Therefore we applied selected kinds of algae in the field, some areas were liming, and the field has been monitoring and sampling during next three years. The results show that the application of dolomitic limestone does not affect progress of biological crusts. The result of the fluorescent microscopy clearly shows, that Klebsormidium algae was the only one of the tested algae, which survived and progressed compact visible crusts.

Heaps of fire-cracked stone is an archaeological site category frequently found in Sweden. The heaps were constructed by piling a massive amount of deposited fire-cracked stones and occasionally they contain artefacts, for example, grindstones, ceramics or bones from both humans and animals. The heaps are sometimes also constructed with complex inner stone patterns in forms of e.g. circles and spirals. The heaps have been found all over Sweden, but the largest concentration is associated with the county of Uppland, north of Stockholm in eastern Sweden. In general, the structures have been linked chronologically to the Bronze Age (1800 B.C.–500 B.C.), although the heaps might be one of the least understood features of Scandinavian prehistory, as a result of their complex and varying content and spatial location. The remains are thoroughly debated, and the interpretation of them varies, ranging from graves to household indications, from sacral to profane, from piles of waste to markers of claimed land. The interpretations of the fire cracked stone heaps have mainly been made by comparing the contents of the heaps with finds from the surrounding archaeological landscape.                  In this study, the heaps will be analysed by using a landscape perspective by which they will be examined in relation to dynamic high-resolution shoreline reconstructions, vegetation and local topography. By examining the heaps by applying a high-resolution landscape model, suggests that their placement patterns are strongly connected to past shorelines. The analysis has in turn resulted in a non-prejudicial dating method for the heaps. The shoreline model was in the next step tested by a comparison to 118 published 14C-dates associated with fire-cracked stone heaps by using Kernel Density Estimations (KDE). The main result of the study is that the high-resolution shoreline model, in combination with KDE, provides an effective dating method for heaps of fire-cracked stone, which in the extension suggests an alternative motive for the construction of the heaps.

The study aims at estimation and mapping the amount of carbon allocated in above ground biomass of wood and in organo-mineral soil horizon at sites where reclamation and spontaneous succession took place on spoil heaps after coal mining. Several categories of data have been used to meet the objectives, namely ground field measurements, laboratory analyses of soil samples, airborne hyperspectral data from VNIR region, and airborne LiDAR scanning data. The digital imagery analysis, GIS modeling and multivariation statistical methods were applied in data assessment. The results show that there is a 7 600 tons of carbon allocated in above ground wood biomass in the area of 209 ha, and 8 100?12 200 tons in the soil A horizon in the region of the same size. The results proofed: 1/ statistically significant negative relationships (p < 0,01) between slope and amount of soil carbon, where higher negative correlation was for broad leaved species; 2/ statistically significant difference (p < 0,05) between amount of soil carbon under broad leaved and needle classes and under different species, the highest between soils under Alnus sp. and Pinus sp.; 3/ statistically significant relationships (p < 0,05) between the amount of carbon allocated in the aboveground wood biomass and that in the soil A horizon under the needle leaved class and under the spontaneous wood vegetation.

Les travaux décrits dans cette thèse portent sur le problème de vérification des systèmes avec espaces d’états infinis, et, en particulier, avec des structures de données chaînées. Plusieurs approches ont émergé, sans donner des solutions convenables et robustes, qui pourrait faire face aux situations rencontrées dans la pratique. Nos travaux proposent une approche nouvelle, qui combine les avantages de deux approches très prometteuses: la représentation symbolique a base d’automates d’arbre, et la logique de séparation. On présente également plusieurs améliorations concernant l’implementation de différentes opérations sur les automates d’arbre, requises pour le succès pratique de notre méthode. En particulier, on propose un algorithme optimise pour le calcul des simulations sur les systèmes de transitions étiquettes, qui se traduit dans un algorithme efficace pour le calcul des simulations sur les automates d’arbre. En outre, on présente un nouvel algorithme pour le problème d’inclusion sur les automates d’arbre. Un nombre important d’expérimentes montre que cet algorithme est plus efficace que certaines des méthodes existantes. / 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 that the new algorithm outperforms other existing approaches.